Theorems · Theorem · commutative algebra
Algebra.isAlgebraic_adjoin_singleton_iff
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R]
{s : S}, R[s].IsAlgebraic ↔ IsAlgebraic R sIn an algebra generated by a single algebraic element over a domain R, every element is
algebraic. This may fail when R is not a domain: see https://mathoverflow.net/a/132192/ for
an example.
- Defined in
- Mathlib.RingTheory.Algebraic.Integral
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 140 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- NoZeroDivisorsstatement and proof · cited by 545
- Algebra.adjoinstatement · cited by 535
- IsAlgebraicstatement · cited by 163
- Set.singleton_nonemptyproof · cited by 32
- Subalgebra.IsAlgebraicstatement · cited by 6
- Algebra.isAlgebraic_adjoin_of_nonemptyproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- IsAlgebraic.of_mulproof · cited by 4