doc-next-gen

Mathlib.RingTheory.Algebraic.Basic

Module docstring

{"# Algebraic elements and algebraic extensions

An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial. An R-algebra is algebraic over R if and only if all its elements are algebraic over R. The main result in this file proves transitivity of algebraicity: a tower of algebraic field extensions is algebraic. "}

is_transcendental_of_subsingleton theorem
[Subsingleton R] (x : A) : Transcendental R x
Full source 
@[nontriviality]
theorem is_transcendental_of_subsingleton [Subsingleton R] (x : A) : Transcendental R x :=
  fun ⟨p, h, _⟩ => h <| Subsingleton.elim p 0
Transcendental Elements over Subsingleton Rings
Informal description
If the ring $R$ is a subsingleton (i.e., has at most one element), then every element $x$ in an $R$-algebra $A$ is transcendental over $R$.
Algebra.IsAlgebraic.nontrivial theorem
[alg : Algebra.IsAlgebraic R A] : Nontrivial R
Full source 
theorem Algebra.IsAlgebraic.nontrivial [alg : Algebra.IsAlgebraic R A] : Nontrivial R :=
  (alg.1 0).nontrivial
Nontriviality of the Base Ring for Algebraic Algebras
Informal description
If an $R$-algebra $A$ is algebraic over $R$ (i.e., every element of $A$ is algebraic over $R$), then the ring $R$ is nontrivial (i.e., contains at least two distinct elements).
Polynomial.transcendental_X theorem
: Transcendental R (X (R := R))
Full source 
theorem Polynomial.transcendental_X : Transcendental R (X (R := R)) := by
  simp [transcendental_iff]
Transcendence of the Polynomial Variable $X$ over $R$
Informal description
The polynomial variable $X$ in the polynomial ring $R[X]$ is transcendental over $R$.
IsAlgebraic.of_aeval theorem
{r : A} (f : R[X]) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ nonZeroDivisors R) (H : IsAlgebraic R (aeval r f)) : IsAlgebraic R r
Full source 
theorem IsAlgebraic.of_aeval {r : A} (f : R[X]) (hf : f.natDegree ≠ 0)
    (hf' : f.leadingCoeff ∈ nonZeroDivisors R) (H : IsAlgebraic R (aeval r f)) :
    IsAlgebraic R r := by
  obtain ⟨p, h1, h2⟩ := H
  have : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0 := fun h ↦ h1 <| by
    rwa [coeff_comp_degree_mul_degree hf,
      mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
      leadingCoeff_eq_zero] at h
  exact ⟨p.comp f, fun h ↦ this (by simp [h]), by rwa [aeval_comp]⟩
Algebraicity of Element via Polynomial Evaluation
Informal description
Let $R$ be a ring and $A$ an $R$-algebra. For an element $r \in A$ and a polynomial $f \in R[X]$ with nonzero degree and leading coefficient in the non-zero divisors of $R$, if the evaluation of $f$ at $r$ (denoted $\text{aeval}\, r\, f$) is algebraic over $R$, then $r$ itself is algebraic over $R$.
Transcendental.aeval theorem
{r : A} (H : Transcendental R r) (f : R[X]) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ nonZeroDivisors R) : Transcendental R (aeval r f)
Full source 
theorem Transcendental.aeval {r : A} (H : Transcendental R r) (f : R[X]) (hf : f.natDegree ≠ 0)
    (hf' : f.leadingCoeff ∈ nonZeroDivisors R) :
    Transcendental R (aeval r f) := fun h ↦ H (h.of_aeval f hf hf')
Transcendence Preservation under Polynomial Evaluation: $\text{Transcendental}(R, r) \Rightarrow \text{Transcendental}(R, \text{aeval}\, r\, f)$
Informal description
Let $R$ be a ring and $A$ an $R$-algebra. For any element $r \in A$ that is transcendental over $R$, and for any polynomial $f \in R[X]$ with nonzero degree and leading coefficient in the non-zero divisors of $R$, the evaluation $\text{aeval}\, r\, f$ is transcendental over $R$.
Transcendental.aeval_of_transcendental theorem
{r : A} (H : Transcendental R r) {f : R[X]} (hf : Transcendental R f) : Transcendental R (Polynomial.aeval r f)
Full source 
/-- If `r : A` and `f : R[X]` are transcendental over `R`, then `Polynomial.aeval r f` is also
transcendental over `R`. For the converse, see `Transcendental.of_aeval` and
`transcendental_aeval_iff`. -/
theorem Transcendental.aeval_of_transcendental {r : A} (H : Transcendental R r)
    {f : R[X]} (hf : Transcendental R f) : Transcendental R (Polynomial.aeval r f) := by
  rw [transcendental_iff] at H hf ⊢
  intro p hp
  exact hf _ (H _ (by rwa [← aeval_comp, comp_eq_aeval] at hp))
Transcendence Preservation under Polynomial Evaluation: $\text{Transcendental}(R, r) \land \text{Transcendental}(R, f) \Rightarrow \text{Transcendental}(R, \text{aeval}\, r\, f)$
Informal description
Let $A$ be an $R$-algebra and $r \in A$ be transcendental over $R$. For any polynomial $f \in R[X]$ that is transcendental over $R$, the evaluation $\text{aeval}\, r\, f$ is also transcendental over $R$.
Transcendental.of_aeval theorem
{r : A} {f : R[X]} (H : Transcendental R (Polynomial.aeval r f)) : Transcendental R f
Full source 
/-- If `Polynomial.aeval r f` is transcendental over `R`, then `f : R[X]` is also
transcendental over `R`. In fact, the `r` is also transcendental over `R` provided that `R`
is a field (see `transcendental_aeval_iff`). -/
theorem Transcendental.of_aeval {r : A} {f : R[X]}
    (H : Transcendental R (Polynomial.aeval r f)) : Transcendental R f := by
  rw [transcendental_iff] at H ⊢
  intro p hp
  exact H p (by rw [← aeval_comp, comp_eq_aeval, hp, map_zero])
Transcendence of Polynomial Implied by Transcendence of Its Evaluation
Informal description
Let $R$ be a ring and $A$ an $R$-algebra. For any element $r \in A$ and polynomial $f \in R[X]$, if the evaluation $\text{aeval}\, r\, f$ is transcendental over $R$, then $f$ is transcendental over $R$.
IsAlgebraic.of_aeval_of_transcendental theorem
{r : A} {f : R[X]} (H : IsAlgebraic R (aeval r f)) (hf : Transcendental R f) : IsAlgebraic R r
Full source 
theorem IsAlgebraic.of_aeval_of_transcendental {r : A} {f : R[X]}
    (H : IsAlgebraic R (aeval r f)) (hf : Transcendental R f) : IsAlgebraic R r := by
  contrapose H
  exact Transcendental.aeval_of_transcendental H hf
Algebraicity of $r$ from algebraic evaluation of transcendental polynomial
Informal description
Let $A$ be an $R$-algebra, $r \in A$, and $f \in R[X]$. If the evaluation $\text{aeval}\, r\, f$ is algebraic over $R$ and $f$ is transcendental over $R$, then $r$ is algebraic over $R$.
Polynomial.transcendental theorem
(f : R[X]) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ nonZeroDivisors R) : Transcendental R f
Full source 
theorem Polynomial.transcendental (f : R[X]) (hf : f.natDegree ≠ 0)
    (hf' : f.leadingCoeff ∈ nonZeroDivisors R) :
    Transcendental R f := by
  simpa using (transcendental_X R).aeval f hf hf'
Transcendence of Nonconstant Polynomials with Nondivisor-Zero Leading Coefficient
Informal description
Let $R$ be a ring and $f \in R[X]$ a polynomial with nonzero degree and leading coefficient in the non-zero divisors of $R$. Then $f$ is transcendental over $R$.
isAlgebraic_iff_not_injective theorem
{x : A} : IsAlgebraic R x ↔ ¬Function.Injective (Polynomial.aeval x : R[X] →ₐ[R] A)
Full source 
theorem isAlgebraic_iff_not_injective {x : A} :
    IsAlgebraicIsAlgebraic R x ↔ ¬Function.Injective (Polynomial.aeval x : R[X] →ₐ[R] A) := by
  simp only [IsAlgebraic, injective_iff_map_eq_zero, not_forall, and_comm, exists_prop]
Algebraicity Criterion via Non-Injectivity of Evaluation Homomorphism
Informal description
An element $x$ of an $R$-algebra $A$ is algebraic over $R$ if and only if the polynomial evaluation homomorphism $\text{aeval}_x \colon R[X] \to A$ (given by $p \mapsto p(x)$) is not injective.
transcendental_iff_injective theorem
{x : A} : Transcendental R x ↔ Function.Injective (Polynomial.aeval x : R[X] →ₐ[R] A)
Full source 
/-- An element `x` is transcendental over `R` if and only if the map `Polynomial.aeval x`
is injective. This is similar to `algebraicIndependent_iff_injective_aeval`. -/
theorem transcendental_iff_injective {x : A} :
    TranscendentalTranscendental R x ↔ Function.Injective (Polynomial.aeval x : R[X] →ₐ[R] A) :=
  isAlgebraic_iff_not_injective.not_left
Transcendental Element Criterion via Injectivity of Evaluation Homomorphism
Informal description
An element $x$ of an $R$-algebra $A$ is transcendental over $R$ if and only if the polynomial evaluation homomorphism $\text{aeval}_x \colon R[X] \to A$ (given by $p \mapsto p(x)$) is injective.
transcendental_iff_ker_eq_bot theorem
{x : A} : Transcendental R x ↔ RingHom.ker (aeval (R := R) x) = ⊥
Full source 
/-- An element `x` is transcendental over `R` if and only if the kernel of the ring homomorphism
`Polynomial.aeval x` is the zero ideal. This is similar to `algebraicIndependent_iff_ker_eq_bot`. -/
theorem transcendental_iff_ker_eq_bot {x : A} :
    TranscendentalTranscendental R x ↔ RingHom.ker (aeval (R := R) x) = ⊥ := by
  rw [transcendental_iff_injective, RingHom.injective_iff_ker_eq_bot]
Transcendental Element Criterion via Kernel of Evaluation Homomorphism
Informal description
An element $x$ of an $R$-algebra $A$ is transcendental over $R$ if and only if the kernel of the polynomial evaluation homomorphism $\text{aeval}_x \colon R[X] \to A$ (given by $p \mapsto p(x)$) is the zero ideal.
Algebra.isAlgebraic_of_not_injective theorem
(h : ¬Function.Injective (algebraMap R A)) : Algebra.IsAlgebraic R A
Full source 
theorem Algebra.isAlgebraic_of_not_injective (h : ¬ Function.Injective (algebraMap R A)) :
    Algebra.IsAlgebraic R A where
  isAlgebraic a := isAlgebraic_iff_not_injective.mpr
    fun inj ↦ h <| by convert inj.comp C_injective; ext; simp
Non-injective algebra map implies algebraic algebra
Informal description
If the algebra map $\text{algebraMap} \colon R \to A$ is not injective, then the $R$-algebra $A$ is algebraic over $R$, meaning every element of $A$ is algebraic over $R$.
Algebra.injective_of_transcendental theorem
[h : Algebra.Transcendental R A] : Function.Injective (algebraMap R A)
Full source 
theorem Algebra.injective_of_transcendental [h : Algebra.Transcendental R A] :
    Function.Injective (algebraMap R A) := by
  rw [transcendental_iff_not_isAlgebraic] at h
  contrapose! h
  exact isAlgebraic_of_not_injective h
Injectivity of Algebra Map in Transcendental Extensions
Informal description
If an $R$-algebra $A$ is transcendental over $R$ (i.e., contains at least one transcendental element over $R$), then the algebra map $\text{algebraMap} \colon R \to A$ is injective.
isAlgebraic_zero theorem
[Nontrivial R] : IsAlgebraic R (0 : A)
Full source 
theorem isAlgebraic_zero [Nontrivial R] : IsAlgebraic R (0 : A) :=
  ⟨_, X_ne_zero, aeval_X 0⟩
Algebraicity of zero element over a nontrivial ring
Informal description
If $R$ is a nontrivial ring, then the zero element $0$ in an $R$-algebra $A$ is algebraic over $R$.
isAlgebraic_algebraMap theorem
[Nontrivial R] (x : R) : IsAlgebraic R (algebraMap R A x)
Full source 
/-- An element of `R` is algebraic, when viewed as an element of the `R`-algebra `A`. -/
theorem isAlgebraic_algebraMap [Nontrivial R] (x : R) : IsAlgebraic R (algebraMap R A x) :=
  ⟨_, X_sub_C_ne_zero x, by rw [map_sub, aeval_X, aeval_C, sub_self]⟩
Algebraicity of algebra map images over nontrivial rings
Informal description
Let $R$ be a nontrivial ring and $A$ an $R$-algebra. For any element $x \in R$, the image of $x$ under the algebra map $\text{algebraMap} \colon R \to A$ is algebraic over $R$.
isAlgebraic_one theorem
[Nontrivial R] : IsAlgebraic R (1 : A)
Full source 
theorem isAlgebraic_one [Nontrivial R] : IsAlgebraic R (1 : A) := by
  rw [← map_one (algebraMap R A)]
  exact isAlgebraic_algebraMap 1
Algebraicity of the multiplicative identity over a nontrivial ring
Informal description
If $R$ is a nontrivial ring, then the multiplicative identity element $1$ in an $R$-algebra $A$ is algebraic over $R$.
isAlgebraic_nat theorem
[Nontrivial R] (n : ℕ) : IsAlgebraic R (n : A)
Full source 
theorem isAlgebraic_nat [Nontrivial R] (n : ℕ) : IsAlgebraic R (n : A) := by
  rw [← map_natCast (_ : R →+* A) n]
  exact isAlgebraic_algebraMap (Nat.cast n)
Algebraicity of Natural Numbers in Nontrivial Ring Extensions
Informal description
For any nontrivial ring $R$ and any $R$-algebra $A$, every natural number $n$ is algebraic over $R$ when viewed as an element of $A$ via the canonical embedding.
isAlgebraic_int theorem
[Nontrivial R] (n : ℤ) : IsAlgebraic R (n : A)
Full source 
theorem isAlgebraic_int [Nontrivial R] (n : ℤ) : IsAlgebraic R (n : A) := by
  rw [← map_intCast (algebraMap R A)]
  exact isAlgebraic_algebraMap (Int.cast n)
Algebraicity of Integer Images in Nontrivial Ring Algebras
Informal description
For any integer $n \in \mathbb{Z}$ and any nontrivial ring $R$, the image of $n$ in an $R$-algebra $A$ is algebraic over $R$.
isAlgebraic_rat theorem
(R : Type u) {A : Type v} [DivisionRing A] [Field R] [Algebra R A] (n : ℚ) : IsAlgebraic R (n : A)
Full source 
theorem isAlgebraic_rat (R : Type u) {A : Type v} [DivisionRing A] [Field R] [Algebra R A] (n : ℚ) :
    IsAlgebraic R (n : A) := by
  rw [← map_ratCast (algebraMap R A)]
  exact isAlgebraic_algebraMap (Rat.cast n)
Algebraicity of Rational Numbers in Division Ring Algebras
Informal description
Let $R$ be a field and $A$ a division ring with an $R$-algebra structure. For any rational number $n \in \mathbb{Q}$, the element $n$ in $A$ is algebraic over $R$.
isAlgebraic_of_mem_rootSet theorem
{R : Type u} {A : Type v} [CommRing R] [Field A] [Algebra R A] {p : R[X]} {x : A} (hx : x ∈ p.rootSet A) : IsAlgebraic R x
Full source 
theorem isAlgebraic_of_mem_rootSet {R : Type u} {A : Type v} [CommRing R] [Field A] [Algebra R A]
    {p : R[X]} {x : A} (hx : x ∈ p.rootSet A) : IsAlgebraic R x :=
  ⟨p, ne_zero_of_mem_rootSet hx, aeval_eq_zero_of_mem_rootSet hx⟩
Elements in Root Set are Algebraic
Informal description
Let $R$ be a commutative ring and $A$ a field with an $R$-algebra structure. For any polynomial $p \in R[X]$ and any element $x \in A$, if $x$ belongs to the root set of $p$ in $A$ (i.e., $p(x) = 0$), then $x$ is algebraic over $R$.
IsLocalization.isAlgebraic theorem
[Nontrivial R] (M : Submonoid R) [IsLocalization M S] : Algebra.IsAlgebraic R S
Full source 
theorem IsLocalization.isAlgebraic [Nontrivial R] (M : Submonoid R) [IsLocalization M S] :
    Algebra.IsAlgebraic R S where
  isAlgebraic x := by
    obtain rfl | hx := eq_or_ne x 0
    · exact isAlgebraic_zero
    have ⟨⟨r, m⟩, h⟩ := surj M x
    refine ⟨C m.1 * X - C r, fun eq ↦ hx ?_, by simpa [sub_eq_zero, mul_comm x] using h⟩
    rwa [← eq_mk'_iff_mul_eq, show r = 0 by simpa using congr(coeff $eq 0), mk'_zero] at h
Algebraicity of Localization over Base Ring
Informal description
Let $R$ be a nontrivial ring and $M$ a submonoid of $R$. If $S$ is the localization of $R$ at $M$, then every element of $S$ is algebraic over $R$. In other words, the $R$-algebra $S$ is algebraic over $R$.
IsAlgebraic.algebraMap theorem
{a : S} : IsAlgebraic R a → IsAlgebraic R (algebraMap S A a)
Full source 
protected theorem IsAlgebraic.algebraMap {a : S} :
    IsAlgebraic R a → IsAlgebraic R (algebraMap S A a) := fun ⟨f, hf₁, hf₂⟩ =>
  ⟨f, hf₁, by rw [aeval_algebraMap_apply, hf₂, map_zero]⟩
Algebraicity is preserved under canonical algebra homomorphisms
Informal description
Let $R$, $S$, and $A$ be rings with $R$-algebra structures, and let $\phi: S \to A$ be the canonical $R$-algebra homomorphism. For any element $a \in S$ that is algebraic over $R$, its image $\phi(a) \in A$ is also algebraic over $R$.
IsAlgebraic.algHom theorem
(f : A →ₐ[R] B) {a : A} (h : IsAlgebraic R a) : IsAlgebraic R (f a)
Full source 
/-- This is slightly more general than `IsAlgebraic.algebraMap` in that it
  allows noncommutative intermediate rings `A`. -/
protected theorem IsAlgebraic.algHom (f : A →ₐ[R] B) {a : A}
    (h : IsAlgebraic R a) : IsAlgebraic R (f a) :=
  let ⟨p, hp, ha⟩ := h
  ⟨p, hp, by rw [aeval_algHom, f.comp_apply, ha, map_zero]⟩
Algebraicity is preserved under algebra homomorphisms
Informal description
Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. Given an $R$-algebra homomorphism $f \colon A \to B$ and an element $a \in A$ that is algebraic over $R$, the image $f(a) \in B$ is also algebraic over $R$.
isAlgebraic_algHom_iff theorem
(f : A →ₐ[R] B) (hf : Function.Injective f) {a : A} : IsAlgebraic R (f a) ↔ IsAlgebraic R a
Full source 
theorem isAlgebraic_algHom_iff (f : A →ₐ[R] B) (hf : Function.Injective f)
    {a : A} : IsAlgebraicIsAlgebraic R (f a) ↔ IsAlgebraic R a :=
  ⟨fun ⟨p, hp0, hp⟩ ↦ ⟨p, hp0, hf <| by rwa [map_zero, ← f.comp_apply, ← aeval_algHom]⟩,
    IsAlgebraic.algHom f⟩
Algebraicity is Equivalent Under Injective Algebra Homomorphisms
Informal description
Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. Given an injective $R$-algebra homomorphism $f \colon A \to B$ and an element $a \in A$, the image $f(a) \in B$ is algebraic over $R$ if and only if $a$ is algebraic over $R$.
IsAlgebraic.ringHom_of_comp_eq theorem
(halg : IsAlgebraic R a) (hf : Function.Injective f) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : IsAlgebraic S (g a)
Full source 
theorem IsAlgebraic.ringHom_of_comp_eq (halg : IsAlgebraic R a)
    (hf : Function.Injective f)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    IsAlgebraic S (g a) := by
  obtain ⟨p, h1, h2⟩ := halg
  refine ⟨p.map f, (Polynomial.map_ne_zero_iff hf).2 h1, ?_⟩
  change aeval ((g : A →+* B) a) _ = 0
  rw [← map_aeval_eq_aeval_map h, h2, map_zero]
Algebraicity is preserved under ring homomorphisms with commutative diagram
Informal description
Let $R$ and $S$ be commutative rings, and let $A$ be an $R$-algebra and $B$ an $S$-algebra. Given: 1. An element $a \in A$ that is algebraic over $R$, 2. An injective ring homomorphism $f: A \to B$, 3. A ring homomorphism $g: R \to S$ such that the following diagram commutes: $$\begin{array}{ccc} R & \xrightarrow{\text{algebraMap}} & A \\ g \downarrow & & \downarrow f \\ S & \xrightarrow{\text{algebraMap}} & B \end{array}$$ then the element $g(a) \in B$ is algebraic over $S$.
Transcendental.of_ringHom_of_comp_eq theorem
(H : Transcendental S (g a)) (hf : Function.Injective f) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Transcendental R a
Full source 
theorem Transcendental.of_ringHom_of_comp_eq (H : Transcendental S (g a))
    (hf : Function.Injective f)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Transcendental R a := fun halg ↦ H (halg.ringHom_of_comp_eq f g hf h)
Transcendence is preserved under injective ring homomorphisms with commutative diagram
Informal description
Let $R$ and $S$ be commutative rings, $A$ an $R$-algebra, and $B$ an $S$-algebra. Given: 1. An element $g(a) \in B$ that is transcendental over $S$, 2. An injective ring homomorphism $f \colon A \to B$, 3. A ring homomorphism $g \colon R \to S$ such that the following diagram commutes: $$\begin{array}{ccc} R & \xrightarrow{\text{algebraMap}} & A \\ g \downarrow & & \downarrow f \\ S & \xrightarrow{\text{algebraMap}} & B \end{array}$$ then the element $a \in A$ is transcendental over $R$.
Algebra.IsAlgebraic.ringHom_of_comp_eq theorem
[Algebra.IsAlgebraic R A] (hf : Function.Injective f) (hg : Function.Surjective g) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Algebra.IsAlgebraic S B
Full source 
theorem Algebra.IsAlgebraic.ringHom_of_comp_eq [Algebra.IsAlgebraic R A]
    (hf : Function.Injective f) (hg : Function.Surjective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.IsAlgebraic S B := by
  refine ⟨fun b ↦ ?_⟩
  obtain ⟨a, rfl⟩ := hg b
  exact (Algebra.IsAlgebraic.isAlgebraic a).ringHom_of_comp_eq f g hf h
Transitivity of Algebraicity via Ring Homomorphisms
Informal description
Let $R$ and $S$ be commutative rings, and let $A$ be an $R$-algebra and $B$ an $S$-algebra. Suppose: 1. Every element of $A$ is algebraic over $R$, 2. The ring homomorphism $f: A \to B$ is injective, 3. The ring homomorphism $g: R \to S$ is surjective, and 4. The following diagram commutes: $$\begin{array}{ccc} R & \xrightarrow{\text{algebraMap}} & A \\ g \downarrow & & \downarrow f \\ S & \xrightarrow{\text{algebraMap}} & B \end{array}$$ Then every element of $B$ is algebraic over $S$.
Algebra.Transcendental.of_ringHom_of_comp_eq theorem
[H : Algebra.Transcendental S B] (hf : Function.Injective f) (hg : Function.Surjective g) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Algebra.Transcendental R A
Full source 
theorem Algebra.Transcendental.of_ringHom_of_comp_eq [H : Algebra.Transcendental S B]
    (hf : Function.Injective f) (hg : Function.Surjective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.Transcendental R A := by
  rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢
  exact fun halg ↦ H (halg.ringHom_of_comp_eq f g hf hg h)
Transcendence propagation via injective-surjective ring homomorphisms with commutative diagram
Informal description
Let $R$ and $S$ be commutative rings, $A$ an $R$-algebra, and $B$ an $S$-algebra. Suppose: 1. $B$ is transcendental over $S$ (i.e., contains at least one element transcendental over $S$), 2. The ring homomorphism $f: A \to B$ is injective, 3. The ring homomorphism $g: R \to S$ is surjective, and 4. The following diagram commutes: $$\begin{array}{ccc} R & \xrightarrow{\text{algebraMap}} & A \\ g \downarrow & & \downarrow f \\ S & \xrightarrow{\text{algebraMap}} & B \end{array}$$ Then $A$ is transcendental over $R$ (i.e., contains at least one element transcendental over $R$).
IsAlgebraic.of_ringHom_of_comp_eq theorem
(halg : IsAlgebraic S (g a)) (hf : Function.Surjective f) (hg : Function.Injective g) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : IsAlgebraic R a
Full source 
theorem IsAlgebraic.of_ringHom_of_comp_eq (halg : IsAlgebraic S (g a))
    (hf : Function.Surjective f) (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    IsAlgebraic R a := by
  obtain ⟨p, h1, h2⟩ := halg
  obtain ⟨q, rfl⟩ := map_surjective (f : R →+* S) hf p
  refine ⟨q, fun h' ↦ by simp [h'] at h1, hg ?_⟩
  change aeval ((g : A →+* B) a) _ = 0 at h2
  change (g : A →+* B) _ = _
  rw [map_zero, map_aeval_eq_aeval_map h, h2]
Algebraicity via Commutative Diagram of Ring Homomorphisms
Informal description
Let $R$, $S$, $A$, and $B$ be rings with algebra structures, and let $f: R \to S$ and $g: A \to B$ be ring homomorphisms. Suppose that: 1. The element $g(a) \in B$ is algebraic over $S$, 2. $f$ is surjective, 3. $g$ is injective, and 4. The following diagram commutes: $$ \begin{CD} R @>{f}>> S \\ @V{\text{algebraMap } R A}VV @VV{\text{algebraMap } S B}V \\ A @>{g}>> B \end{CD} $$ Then the element $a \in A$ is algebraic over $R$.
Transcendental.ringHom_of_comp_eq theorem
(H : Transcendental R a) (hf : Function.Surjective f) (hg : Function.Injective g) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Transcendental S (g a)
Full source 
theorem Transcendental.ringHom_of_comp_eq (H : Transcendental R a)
    (hf : Function.Surjective f) (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Transcendental S (g a) := fun halg ↦ H (halg.of_ringHom_of_comp_eq f g hf hg h)
Transcendence via Commutative Diagram of Ring Homomorphisms
Informal description
Let $R$, $S$, $A$, and $B$ be rings with algebra structures, and let $f: R \to S$ and $g: A \to B$ be ring homomorphisms. Suppose that: 1. The element $a \in A$ is transcendental over $R$, 2. $f$ is surjective, 3. $g$ is injective, and 4. The following diagram commutes: $$ \begin{CD} R @>{f}>> S \\ @V{\text{algebraMap } R A}VV @VV{\text{algebraMap } S B}V \\ A @>{g}>> B \end{CD} $$ Then the element $g(a) \in B$ is transcendental over $S$.
Algebra.IsAlgebraic.of_ringHom_of_comp_eq theorem
[Algebra.IsAlgebraic S B] (hf : Function.Surjective f) (hg : Function.Injective g) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Algebra.IsAlgebraic R A
Full source 
theorem Algebra.IsAlgebraic.of_ringHom_of_comp_eq [Algebra.IsAlgebraic S B]
    (hf : Function.Surjective f) (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.IsAlgebraic R A :=
  ⟨fun a ↦ (Algebra.IsAlgebraic.isAlgebraic (g a)).of_ringHom_of_comp_eq f g hf hg h⟩
Transitivity of Algebraicity via Commutative Diagram of Ring Homomorphisms
Informal description
Let $R$, $S$, $A$, and $B$ be rings with algebra structures, and let $f: R \to S$ and $g: A \to B$ be ring homomorphisms. Suppose that: 1. The algebra $B$ is algebraic over $S$, 2. $f$ is surjective, 3. $g$ is injective, and 4. The following diagram commutes: $$ \begin{CD} R @>{f}>> S \\ @V{\text{algebraMap } R A}VV @VV{\text{algebraMap } S B}V \\ A @>{g}>> B \end{CD} $$ Then the algebra $A$ is algebraic over $R$.
Algebra.Transcendental.ringHom_of_comp_eq theorem
[H : Algebra.Transcendental R A] (hf : Function.Surjective f) (hg : Function.Injective g) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Algebra.Transcendental S B
Full source 
theorem Algebra.Transcendental.ringHom_of_comp_eq [H : Algebra.Transcendental R A]
    (hf : Function.Surjective f) (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.Transcendental S B := by
  rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢
  exact fun halg ↦ H (halg.of_ringHom_of_comp_eq f g hf hg h)
Transcendence Transfer via Commutative Diagram of Ring Homomorphisms
Informal description
Let $R$, $S$, $A$, and $B$ be rings with algebra structures, and let $f: R \to S$ and $g: A \to B$ be ring homomorphisms. Suppose that: 1. The algebra $A$ is transcendental over $R$, 2. $f$ is surjective, 3. $g$ is injective, and 4. The following diagram commutes: $$ \begin{CD} R @>{f}>> S \\ @V{\text{algebraMap } R A}VV @VV{\text{algebraMap } S B}V \\ A @>{g}>> B \end{CD} $$ Then the algebra $B$ is transcendental over $S$.
isAlgebraic_ringHom_iff_of_comp_eq theorem
(hg : Function.Injective g) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) {a : A} : IsAlgebraic S (g a) ↔ IsAlgebraic R a
Full source 
theorem isAlgebraic_ringHom_iff_of_comp_eq
    (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) {a : A} :
    IsAlgebraicIsAlgebraic S (g a) ↔ IsAlgebraic R a :=
  ⟨fun H ↦ H.of_ringHom_of_comp_eq f g (EquivLike.surjective f) hg h,
    fun H ↦ H.ringHom_of_comp_eq f g (EquivLike.injective f) h⟩
Algebraicity Equivalence under Commutative Diagram of Ring Homomorphisms
Informal description
Let $R$ and $S$ be commutative rings, and let $A$ be an $R$-algebra and $B$ an $S$-algebra. Given injective ring homomorphisms $f: R \to S$ and $g: A \to B$ such that the following diagram commutes: $$ \begin{CD} R @>{f}>> S \\ @V{\text{algebraMap } R A}VV @VV{\text{algebraMap } S B}V \\ A @>{g}>> B \end{CD} $$ then for any element $a \in A$, $g(a)$ is algebraic over $S$ if and only if $a$ is algebraic over $R$.
transcendental_ringHom_iff_of_comp_eq theorem
(hg : Function.Injective g) (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) {a : A} : Transcendental S (g a) ↔ Transcendental R a
Full source 
theorem transcendental_ringHom_iff_of_comp_eq
    (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) {a : A} :
    TranscendentalTranscendental S (g a) ↔ Transcendental R a :=
  not_congr (isAlgebraic_ringHom_iff_of_comp_eq f g hg h)
Transcendence Equivalence under Commutative Diagram of Ring Homomorphisms
Informal description
Let $R$ and $S$ be commutative rings, and let $A$ be an $R$-algebra and $B$ an $S$-algebra. Given injective ring homomorphisms $f: R \to S$ and $g: A \to B$ such that the following diagram commutes: $$ \begin{CD} R @>{f}>> S \\ @V{\text{algebraMap } R A}VV @VV{\text{algebraMap } S B}V \\ A @>{g}>> B \end{CD} $$ then for any element $a \in A$, $g(a)$ is transcendental over $S$ if and only if $a$ is transcendental over $R$.
Algebra.isAlgebraic_ringHom_iff_of_comp_eq theorem
(h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Algebra.IsAlgebraic S B ↔ Algebra.IsAlgebraic R A
Full source 
theorem Algebra.isAlgebraic_ringHom_iff_of_comp_eq
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.IsAlgebraicAlgebra.IsAlgebraic S B ↔ Algebra.IsAlgebraic R A :=
  ⟨fun H ↦ H.of_ringHom_of_comp_eq f g (EquivLike.surjective f) (EquivLike.injective g) h,
    fun H ↦ H.ringHom_of_comp_eq f g (EquivLike.injective f) (EquivLike.surjective g) h⟩
Algebraicity Equivalence Under Commuting Ring Homomorphisms
Informal description
Let $R$ and $S$ be commutative rings, with $A$ an $R$-algebra and $B$ an $S$-algebra. Given ring homomorphisms $f: R \to S$ and $g: A \to B$ such that the following diagram commutes: $$ \begin{CD} R @>{f}>> S \\ @V{\text{algebraMap } R A}VV @VV{\text{algebraMap } S B}V \\ A @>{g}>> B \end{CD} $$ then $B$ is algebraic over $S$ if and only if $A$ is algebraic over $R$.
Algebra.transcendental_ringHom_iff_of_comp_eq theorem
(h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Algebra.Transcendental S B ↔ Algebra.Transcendental R A
Full source 
theorem Algebra.transcendental_ringHom_iff_of_comp_eq
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    Algebra.TranscendentalAlgebra.Transcendental S B ↔ Algebra.Transcendental R A := by
  simp_rw [Algebra.transcendental_iff_not_isAlgebraic,
    Algebra.isAlgebraic_ringHom_iff_of_comp_eq f g h]
Transcendence Equivalence Under Commuting Ring Homomorphisms
Informal description
Let $R$ and $S$ be commutative rings, with $A$ an $R$-algebra and $B$ an $S$-algebra. Given ring homomorphisms $f: R \to S$ and $g: A \to B$ such that the following diagram commutes: $$ \begin{CD} R @>{f}>> S \\ @V{\text{algebraMap } R A}VV @VV{\text{algebraMap } S B}V \\ A @>{g}>> B \end{CD} $$ then $B$ is transcendental over $S$ if and only if $A$ is transcendental over $R$.
Algebra.IsAlgebraic.of_injective theorem
(f : A →ₐ[R] B) (hf : Function.Injective f) [Algebra.IsAlgebraic R B] : Algebra.IsAlgebraic R A
Full source 
theorem Algebra.IsAlgebraic.of_injective (f : A →ₐ[R] B) (hf : Function.Injective f)
    [Algebra.IsAlgebraic R B] : Algebra.IsAlgebraic R A :=
  ⟨fun _ ↦ (isAlgebraic_algHom_iff f hf).mp (Algebra.IsAlgebraic.isAlgebraic _)⟩
Injective Algebra Homomorphism Preserves Algebraicity
Informal description
Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. Given an injective $R$-algebra homomorphism $f \colon A \to B$, if $B$ is algebraic over $R$, then $A$ is algebraic over $R$.
AlgEquiv.isAlgebraic theorem
(e : A ≃ₐ[R] B) [Algebra.IsAlgebraic R A] : Algebra.IsAlgebraic R B
Full source 
/-- Transfer `Algebra.IsAlgebraic` across an `AlgEquiv`. -/
theorem AlgEquiv.isAlgebraic (e : A ≃ₐ[R] B)
    [Algebra.IsAlgebraic R A] : Algebra.IsAlgebraic R B :=
  Algebra.IsAlgebraic.of_injective e.symm.toAlgHom e.symm.injective
Algebra Equivalence Preserves Algebraicity
Informal description
Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. Given an algebra equivalence $e \colon A \simeq B$ and assuming $A$ is algebraic over $R$, then $B$ is algebraic over $R$.
AlgEquiv.isAlgebraic_iff theorem
(e : A ≃ₐ[R] B) : Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R B
Full source 
theorem AlgEquiv.isAlgebraic_iff (e : A ≃ₐ[R] B) :
    Algebra.IsAlgebraicAlgebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R B :=
  ⟨fun _ ↦ e.isAlgebraic, fun _ ↦ e.symm.isAlgebraic⟩
Algebra Equivalence Preserves Algebraicity (Bidirectional)
Informal description
Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. Given an algebra equivalence $e \colon A \simeq B$, the algebra $A$ is algebraic over $R$ if and only if $B$ is algebraic over $R$.
isAlgebraic_algebraMap_iff theorem
{a : S} (h : Function.Injective (algebraMap S A)) : IsAlgebraic R (algebraMap S A a) ↔ IsAlgebraic R a
Full source 
theorem isAlgebraic_algebraMap_iff {a : S} (h : Function.Injective (algebraMap S A)) :
    IsAlgebraicIsAlgebraic R (algebraMap S A a) ↔ IsAlgebraic R a :=
  isAlgebraic_algHom_iff (IsScalarTower.toAlgHom R S A) h
Algebraicity is Equivalent Under Injective Algebra Maps
Informal description
Let $R$ be a commutative ring, and let $S$ and $A$ be $R$-algebras. Suppose the algebra map $\text{algebraMap} \colon S \to A$ is injective. Then for any element $a \in S$, the image $\text{algebraMap}(a) \in A$ is algebraic over $R$ if and only if $a$ is algebraic over $R$.
transcendental_algebraMap_iff theorem
{a : S} (h : Function.Injective (algebraMap S A)) : Transcendental R (algebraMap S A a) ↔ Transcendental R a
Full source 
theorem transcendental_algebraMap_iff {a : S} (h : Function.Injective (algebraMap S A)) :
    TranscendentalTranscendental R (algebraMap S A a) ↔ Transcendental R a := by
  simp_rw [Transcendental, isAlgebraic_algebraMap_iff h]
Transcendence is Equivalent Under Injective Algebra Maps
Informal description
Let $R$ be a commutative ring, and let $S$ and $A$ be $R$-algebras. Suppose the algebra map $\text{algebraMap} \colon S \to A$ is injective. Then for any element $a \in S$, the image $\text{algebraMap}(a) \in A$ is transcendental over $R$ if and only if $a$ is transcendental over $R$.
Subalgebra.isAlgebraic_iff_isAlgebraic_val theorem
{S : Subalgebra R A} {x : S} : _root_.IsAlgebraic R x ↔ _root_.IsAlgebraic R x.1
Full source 
theorem isAlgebraic_iff_isAlgebraic_val {S : Subalgebra R A} {x : S} :
    _root_.IsAlgebraic_root_.IsAlgebraic R x ↔ _root_.IsAlgebraic R x.1 :=
  (isAlgebraic_algHom_iff S.val Subtype.val_injective).symm
Algebraicity in Subalgebra Equivalent to Algebraicity in Base Algebra
Informal description
Let $S$ be a subalgebra of an $R$-algebra $A$, and let $x \in S$. Then $x$ is algebraic over $R$ if and only if its underlying element $x.1 \in A$ is algebraic over $R$.
Subalgebra.isAlgebraic_of_isAlgebraic_bot theorem
{x : S} (halg : _root_.IsAlgebraic (⊥ : Subalgebra R S) x) : _root_.IsAlgebraic R x
Full source 
theorem isAlgebraic_of_isAlgebraic_bot {x : S} (halg : _root_.IsAlgebraic (⊥ : Subalgebra R S) x) :
    _root_.IsAlgebraic R x :=
  halg.of_ringHom_of_comp_eq (algebraMap R (⊥ : Subalgebra R S))
    (RingHom.id S) (by rintro ⟨_, r, rfl⟩; exact ⟨r, rfl⟩) Function.injective_id rfl
Algebraicity over Base Ring from Algebraicity over Bottom Subalgebra
Informal description
Let $S$ be a subalgebra of an $R$-algebra $A$, and let $x \in S$. If $x$ is algebraic over the bottom subalgebra $\bot$ (the smallest subalgebra containing $R$), then $x$ is algebraic over $R$.
Subalgebra.isAlgebraic_bot_iff theorem
(h : Function.Injective (algebraMap R S)) {x : S} : _root_.IsAlgebraic (⊥ : Subalgebra R S) x ↔ _root_.IsAlgebraic R x
Full source 
theorem isAlgebraic_bot_iff (h : Function.Injective (algebraMap R S)) {x : S} :
    _root_.IsAlgebraic_root_.IsAlgebraic (⊥ : Subalgebra R S) x ↔ _root_.IsAlgebraic R x :=
  isAlgebraic_ringHom_iff_of_comp_eq (Algebra.botEquivOfInjective h).symm (RingHom.id S)
    Function.injective_id (by rfl)
Algebraicity over Base Ring vs. Bottom Subalgebra
Informal description
Let $S$ be an $R$-algebra with an injective algebra map $\text{algebraMap } R S$. For any element $x \in S$, $x$ is algebraic over the bottom subalgebra $\bot$ (the smallest subalgebra containing $R$) if and only if $x$ is algebraic over $R$.
Subalgebra.algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left theorem
[Algebra.IsAlgebraic (⊥ : Subalgebra R S) S] : Algebra.IsAlgebraic R S
Full source 
theorem algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left
    [Algebra.IsAlgebraic (⊥ : Subalgebra R S) S] : Algebra.IsAlgebraic R S :=
  Algebra.IsAlgebraic.of_ringHom_of_comp_eq (algebraMap R (⊥ : Subalgebra R S))
    (RingHom.id S) (by rintro ⟨_, r, rfl⟩; exact ⟨r, rfl⟩) Function.injective_id (by ext; rfl)
Algebraicity over Base Ring from Algebraicity over Bottom Subalgebra
Informal description
Let $S$ be an $R$-algebra. If $S$ is algebraic over the bottom subalgebra $\bot$ (the smallest subalgebra containing $R$), then $S$ is algebraic over $R$.
Subalgebra.algebra_isAlgebraic_bot_left_iff theorem
(h : Function.Injective (algebraMap R S)) : Algebra.IsAlgebraic (⊥ : Subalgebra R S) S ↔ Algebra.IsAlgebraic R S
Full source 
theorem algebra_isAlgebraic_bot_left_iff (h : Function.Injective (algebraMap R S)) :
    Algebra.IsAlgebraicAlgebra.IsAlgebraic (⊥ : Subalgebra R S) S ↔ Algebra.IsAlgebraic R S := by
  simp_rw [Algebra.isAlgebraic_def, isAlgebraic_bot_iff h]
Equivalence of Algebraicity over Base Ring and Bottom Subalgebra
Informal description
Let $S$ be an $R$-algebra with an injective algebra map from $R$ to $S$. Then $S$ is algebraic over the bottom subalgebra $\bot$ (the smallest subalgebra containing $R$) if and only if $S$ is algebraic over $R$.
IsAlgebraic.of_pow theorem
{r : A} {n : ℕ} (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) : IsAlgebraic R r
Full source 
theorem IsAlgebraic.of_pow {r : A} {n : ℕ} (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) :
    IsAlgebraic R r :=
  have ⟨p, p_nonzero, hp⟩ := ht
  ⟨_, by rwa [expand_ne_zero hn], by rwa [expand_aeval n p r]⟩
Algebraicity of Roots of Algebraic Elements
Informal description
Let $R$ be a ring and $A$ an $R$-algebra. For any element $r \in A$ and positive integer $n$, if $r^n$ is algebraic over $R$, then $r$ is algebraic over $R$.
Transcendental.pow theorem
{r : A} (ht : Transcendental R r) {n : ℕ} (hn : 0 < n) : Transcendental R (r ^ n)
Full source 
theorem Transcendental.pow {r : A} (ht : Transcendental R r) {n : ℕ} (hn : 0 < n) :
    Transcendental R (r ^ n) := fun ht' ↦ ht <| ht'.of_pow hn
Transcendence of Powers of Transcendental Elements
Informal description
Let $R$ be a ring and $A$ an $R$-algebra. For any element $r \in A$ that is transcendental over $R$ and any positive integer $n$, the power $r^n$ is also transcendental over $R$.
IsAlgebraic.invOf theorem
{x : S} [Invertible x] (h : IsAlgebraic R x) : IsAlgebraic R (⅟ x)
Full source 
lemma IsAlgebraic.invOf {x : S} [Invertible x] (h : IsAlgebraic R x) : IsAlgebraic R (⅟ x) := by
  obtain ⟨p, hp, hp'⟩ := h
  refine ⟨p.reverse, by simpa using hp, ?_⟩
  rwa [Polynomial.aeval_def, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.aeval_def]
Algebraicity of the Inverse of an Algebraic Element
Informal description
Let $R$ be a ring and $S$ an $R$-algebra. For any invertible element $x \in S$, if $x$ is algebraic over $R$, then its multiplicative inverse $⅟x$ is also algebraic over $R$.
IsAlgebraic.inv_iff theorem
{K} [Field K] [Algebra R K] {x : K} : IsAlgebraic R (x⁻¹) ↔ IsAlgebraic R x
Full source 
lemma IsAlgebraic.inv_iff {K} [Field K] [Algebra R K] {x : K} :
    IsAlgebraicIsAlgebraic R (x⁻¹) ↔ IsAlgebraic R x := by
  by_cases hx : x = 0
  · simp [hx]
  letI := invertibleOfNonzero hx
  exact IsAlgebraic.invOf_iff (R := R) (x := x)
Algebraicity of Field Element and Its Inverse
Informal description
Let $R$ be a ring and $K$ a field with an $R$-algebra structure. For any element $x \in K$, the multiplicative inverse $x^{-1}$ is algebraic over $R$ if and only if $x$ itself is algebraic over $R$.
IsAlgebraic.extendScalars theorem
(hinj : Function.Injective (algebraMap R S)) {x : A} (A_alg : IsAlgebraic R x) : IsAlgebraic S x
Full source 
/-- If `x` is algebraic over `R`, then `x` is algebraic over `S` when `S` is an extension of `R`,
  and the map from `R` to `S` is injective. -/
theorem IsAlgebraic.extendScalars (hinj : Function.Injective (algebraMap R S)) {x : A}
    (A_alg : IsAlgebraic R x) : IsAlgebraic S x :=
  let ⟨p, hp₁, hp₂⟩ := A_alg
  ⟨p.map (algebraMap _ _), by
    rwa [Ne, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot], by simpa⟩
Algebraicity is preserved under extension of scalars via an injective map
Informal description
Let $R$ and $S$ be rings with an injective ring homomorphism $R \hookrightarrow S$, and let $A$ be an $S$-algebra. If an element $x \in A$ is algebraic over $R$, then $x$ is also algebraic over $S$.
IsAlgebraic.tower_top_of_subalgebra_le theorem
{A B : Subalgebra R S} (hle : A ≤ B) {x : S} (h : IsAlgebraic A x) : IsAlgebraic B x
Full source 
/-- A special case of `IsAlgebraic.extendScalars`. This is extracted as a theorem
  because in some cases `IsAlgebraic.extendScalars` will just runs out of memory. -/
theorem IsAlgebraic.tower_top_of_subalgebra_le
    {A B : Subalgebra R S} (hle : A ≤ B) {x : S}
    (h : IsAlgebraic A x) : IsAlgebraic B x := by
  letI : Algebra A B := (Subalgebra.inclusion hle).toAlgebra
  haveI : IsScalarTower A B S := .of_algebraMap_eq fun _ ↦ rfl
  exact h.extendScalars (Subalgebra.inclusion_injective hle)
Algebraicity is preserved under subalgebra extension
Informal description
Let $R$ be a ring and $S$ an $R$-algebra. For any two subalgebras $A$ and $B$ of $S$ with $A \subseteq B$, if an element $x \in S$ is algebraic over $A$, then $x$ is also algebraic over $B$.
Transcendental.restrictScalars theorem
(hinj : Function.Injective (algebraMap R S)) {x : A} (h : Transcendental S x) : Transcendental R x
Full source 
/-- If `x` is transcendental over `S`, then `x` is transcendental over `R` when `S` is an extension
  of `R`, and the map from `R` to `S` is injective. -/
theorem Transcendental.restrictScalars (hinj : Function.Injective (algebraMap R S)) {x : A}
    (h : Transcendental S x) : Transcendental R x := fun H ↦ h (H.extendScalars hinj)
Transcendence is preserved under restriction of scalars via an injective map
Informal description
Let $R$ and $S$ be rings with an injective ring homomorphism $R \hookrightarrow S$, and let $A$ be an $S$-algebra. If an element $x \in A$ is transcendental over $S$, then $x$ is also transcendental over $R$.
Transcendental.of_tower_top_of_subalgebra_le theorem
{A B : Subalgebra R S} (hle : A ≤ B) {x : S} (h : Transcendental B x) : Transcendental A x
Full source 
/-- A special case of `Transcendental.restrictScalars`. This is extracted as a theorem
  because in some cases `Transcendental.restrictScalars` will just runs out of memory. -/
theorem Transcendental.of_tower_top_of_subalgebra_le
    {A B : Subalgebra R S} (hle : A ≤ B) {x : S}
    (h : Transcendental B x) : Transcendental A x :=
  fun H ↦ h (H.tower_top_of_subalgebra_le hle)
Transcendence is preserved under subalgebra restriction
Informal description
Let $R$ be a ring and $S$ an $R$-algebra. For any two subalgebras $A$ and $B$ of $S$ with $A \subseteq B$, if an element $x \in S$ is transcendental over $B$, then $x$ is also transcendental over $A$.
Algebra.IsAlgebraic.extendScalars theorem
(hinj : Function.Injective (algebraMap R S)) [Algebra.IsAlgebraic R A] : Algebra.IsAlgebraic S A
Full source 
/-- If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R,
  and the map from `R` to `S` is injective. -/
theorem Algebra.IsAlgebraic.extendScalars (hinj : Function.Injective (algebraMap R S))
    [Algebra.IsAlgebraic R A] : Algebra.IsAlgebraic S A :=
  ⟨fun _ ↦ _root_.IsAlgebraic.extendScalars hinj (Algebra.IsAlgebraic.isAlgebraic _)⟩
Algebraicity is preserved under extension of scalars via an injective map
Informal description
Let $R$ and $S$ be rings with an injective ring homomorphism $R \hookrightarrow S$, and let $A$ be an $S$-algebra. If $A$ is algebraic over $R$, then $A$ is also algebraic over $S$.
Algebra.IsAlgebraic.tower_bot_of_injective theorem
[Algebra.IsAlgebraic R A] (hinj : Function.Injective (algebraMap S A)) : Algebra.IsAlgebraic R S
Full source 
theorem Algebra.IsAlgebraic.tower_bot_of_injective [Algebra.IsAlgebraic R A]
    (hinj : Function.Injective (algebraMap S A)) :
    Algebra.IsAlgebraic R S where
  isAlgebraic x := by
    simpa [isAlgebraic_algebraMap_iff hinj] using isAlgebraic (R := R) (A := A) (algebraMap _ _ x)
Algebraicity of Base Algebra in Tower with Injective Map
Informal description
Let $R$ be a ring, $S$ and $A$ be $R$-algebras. If $A$ is algebraic over $R$ and the algebra map $\text{algebraMap} \colon S \to A$ is injective, then $S$ is algebraic over $R$.
IsAlgebraic.tower_top theorem
{x : A} (A_alg : IsAlgebraic K x) : IsAlgebraic L x
Full source 
/-- If `x` is algebraic over `K`, then `x` is algebraic over `L` when `L` is an extension of `K` -/
@[stacks 09GF "part one"]
theorem IsAlgebraic.tower_top {x : A} (A_alg : IsAlgebraic K x) :
    IsAlgebraic L x :=
  A_alg.extendScalars (algebraMap K L).injective
Algebraicity in Tower Extension: Algebraic Elements over Base Field Remain Algebraic over Extension Field
Informal description
Let $K$ be a field and $L$ be a field extension of $K$. For any element $x$ in an $L$-algebra $A$, if $x$ is algebraic over $K$, then $x$ is also algebraic over $L$.
Transcendental.of_tower_top theorem
{x : A} (h : Transcendental L x) : Transcendental K x
Full source 
/-- If `x` is transcendental over `L`, then `x` is transcendental over `K` when
  `L` is an extension of `K` -/
theorem Transcendental.of_tower_top {x : A} (h : Transcendental L x) :
    Transcendental K x := fun H ↦ h (H.tower_top L)
Transcendental Elements Remain Transcendental in Base Field
Informal description
Let $K$ be a field and $L$ be a field extension of $K$. For any element $x$ in an $L$-algebra $A$, if $x$ is transcendental over $L$, then $x$ is also transcendental over $K$.
Algebra.IsAlgebraic.tower_top theorem
[Algebra.IsAlgebraic K A] : Algebra.IsAlgebraic L A
Full source 
/-- If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K -/
@[stacks 09GF "part two"]
theorem Algebra.IsAlgebraic.tower_top [Algebra.IsAlgebraic K A] : Algebra.IsAlgebraic L A :=
  Algebra.IsAlgebraic.extendScalars (algebraMap K L).injective
Algebraicity is preserved under field extensions
Informal description
Let $K$ be a field and $L$ be an extension field of $K$. If $A$ is an $L$-algebra that is algebraic over $K$, then $A$ is also algebraic over $L$.
Algebra.IsAlgebraic.tower_bot theorem
(K L A : Type*) [CommRing K] [Field L] [Ring A] [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] [Nontrivial A] [Algebra.IsAlgebraic K A] : Algebra.IsAlgebraic K L
Full source 
theorem Algebra.IsAlgebraic.tower_bot (K L A : Type*) [CommRing K] [Field L] [Ring A]
    [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A]
    [Nontrivial A] [Algebra.IsAlgebraic K A] :
    Algebra.IsAlgebraic K L :=
  tower_bot_of_injective (algebraMap L A).injective
Transitivity of Algebraicity in Tower of Extensions: Base Case
Informal description
Let $K$ be a commutative ring, $L$ a field, and $A$ a ring, with $K \to L \to A$ forming a tower of algebra extensions (i.e., $A$ is an $L$-algebra and $L$ is a $K$-algebra, with compatible scalar multiplication). Suppose $A$ is nontrivial and algebraic over $K$. Then $L$ is algebraic over $K$.
Algebra.IsAlgebraic.algHom_bijective theorem
[NoZeroSMulDivisors K L] [Algebra.IsAlgebraic K L] (f : L →ₐ[K] L) : Function.Bijective f
Full source 
theorem algHom_bijective [NoZeroSMulDivisors K L] [Algebra.IsAlgebraic K L] (f : L →ₐ[K] L) :
    Function.Bijective f := by
  refine ⟨f.injective, fun b ↦ ?_⟩
  obtain ⟨p, hp, he⟩ := Algebra.IsAlgebraic.isAlgebraic (R := K) b
  let f' : p.rootSet L → p.rootSet L := (rootSet_maps_to' (fun x ↦ x) f).restrict f _ _
  have : f'.Surjective := Finite.injective_iff_surjective.1
    fun _ _ h ↦ Subtype.eq <| f.injective <| Subtype.ext_iff.1 h
  obtain ⟨a, ha⟩ := this ⟨b, mem_rootSet.2 ⟨hp, he⟩⟩
  exact ⟨a, Subtype.ext_iff.1 ha⟩
Bijectivity of Algebra Homomorphisms in Algebraic Extensions
Informal description
Let $K$ be a commutative ring and $L$ be a field extension of $K$ such that $L$ is algebraic over $K$ and there are no zero scalar divisors between $K$ and $L$. Then every $K$-algebra homomorphism $f \colon L \to L$ is bijective.
Algebra.IsAlgebraic.algHom_bijective₂ theorem
[NoZeroSMulDivisors K L] [DivisionRing R] [Algebra K R] [Algebra.IsAlgebraic K L] (f : L →ₐ[K] R) (g : R →ₐ[K] L) : Function.Bijective f ∧ Function.Bijective g
Full source 
theorem algHom_bijective₂ [NoZeroSMulDivisors K L] [DivisionRing R] [Algebra K R]
    [Algebra.IsAlgebraic K L] (f : L →ₐ[K] R) (g : R →ₐ[K] L) :
    Function.BijectiveFunction.Bijective f ∧ Function.Bijective g :=
  (g.injective.bijective₂_of_surjective f.injective (algHom_bijective <| g.comp f).2).symm
Bijectivity of Paired Algebra Homomorphisms in Algebraic Extensions over Division Rings
Informal description
Let $K$ be a commutative ring and $L$ be a field extension of $K$ such that $L$ is algebraic over $K$ and there are no zero scalar divisors between $K$ and $L$. Let $R$ be a division ring with a $K$-algebra structure. For any $K$-algebra homomorphisms $f \colon L \to R$ and $g \colon R \to L$, both $f$ and $g$ are bijective.
Algebra.IsAlgebraic.bijective_of_isScalarTower theorem
[NoZeroSMulDivisors K L] [Algebra.IsAlgebraic K L] [DivisionRing R] [Algebra K R] [Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L) : Function.Bijective f
Full source 
theorem bijective_of_isScalarTower [NoZeroSMulDivisors K L] [Algebra.IsAlgebraic K L]
    [DivisionRing R] [Algebra K R] [Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L) :
    Function.Bijective f :=
  (algHom_bijective₂ (IsScalarTower.toAlgHom K L R) f).2
Bijectivity of $K$-algebra homomorphisms in algebraic scalar tower extensions over division rings
Informal description
Let $K$ be a commutative ring and $L$ be a field extension of $K$ such that $L$ is algebraic over $K$ and there are no zero scalar divisors between $K$ and $L$. Let $R$ be a division ring with a $K$-algebra structure, and suppose $R$ is also an $L$-algebra forming a scalar tower $K \subseteq L \subseteq R$. Then any $K$-algebra homomorphism $f \colon R \to L$ is bijective.
Algebra.IsAlgebraic.bijective_of_isScalarTower' theorem
[Field R] [Algebra K R] [NoZeroSMulDivisors K R] [Algebra.IsAlgebraic K R] [Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L) : Function.Bijective f
Full source 
theorem bijective_of_isScalarTower' [Field R] [Algebra K R]
    [NoZeroSMulDivisors K R]
    [Algebra.IsAlgebraic K R] [Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L) :
    Function.Bijective f :=
  (algHom_bijective₂ f (IsScalarTower.toAlgHom K L R)).1
Bijectivity of Algebra Homomorphisms in Algebraic Field Towers
Informal description
Let $K$ be a field, $R$ a field extension of $K$ that is algebraic over $K$ with no zero scalar divisors between $K$ and $R$, and $L$ another field extension of $K$ such that $R$ is also an $L$-algebra forming a scalar tower $K \subseteq L \subseteq R$. Then any $K$-algebra homomorphism $f \colon R \to L$ is bijective.
Algebra.IsAlgebraic.algEquivEquivAlgHom definition
[NoZeroSMulDivisors K L] [Algebra.IsAlgebraic K L] : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L)
Full source 
/-- Bijection between algebra equivalences and algebra homomorphisms -/
@[simps]
noncomputable def algEquivEquivAlgHom [NoZeroSMulDivisors K L] [Algebra.IsAlgebraic K L] :
    (L ≃ₐ[K] L) ≃* (L →ₐ[K] L) where
  toFun ϕ := ϕ.toAlgHom
  invFun ϕ := AlgEquiv.ofBijective ϕ (algHom_bijective ϕ)
  left_inv _ := by ext; rfl
  right_inv _ := by ext; rfl
  map_mul' _ _ := rfl
Bijection between algebra automorphisms and algebra homomorphisms in algebraic extensions
Informal description
Given a field extension \( L \) of \( K \) that is algebraic over \( K \) and has no zero scalar divisors, there is a multiplicative bijection between the set of \( K \)-algebra automorphisms of \( L \) (i.e., \( K \)-algebra isomorphisms from \( L \) to itself) and the set of \( K \)-algebra homomorphisms from \( L \) to itself. The bijection maps each automorphism to its underlying homomorphism and constructs an automorphism from any bijective homomorphism.
IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero theorem
{s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) : ∃ q : R[X], q.coeff 0 ≠ 0 ∧ aeval s q = 0
Full source 
theorem IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero
    {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) :
    ∃ q : R[X], q.coeff 0 ≠ 0 ∧ aeval s q = 0 := by
  obtain ⟨p, hp0, hp⟩ := hRs
  obtain ⟨q, hpq, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp0 0
  simp only [C_0, sub_zero, X_pow_mul, X_dvd_iff] at hpq hq
  rw [hpq, map_mul, aeval_X_pow] at hp
  exact ⟨q, hq, (nonZeroDivisors S).pow_mem hs (rootMultiplicity 0 p) (aeval s q) hp⟩
Existence of Nonzero Polynomial with Nonzero Constant Term for Algebraic Non-Zero Divisors
Informal description
Let $R$ be a ring and $S$ an $R$-algebra. For any element $s \in S$ that is algebraic over $R$ and belongs to the non-zero divisors of $S$, there exists a non-zero polynomial $q \in R[X]$ such that the constant term of $q$ is non-zero and $q(s) = 0$ (where $q(s)$ is the evaluation of $q$ at $s$ via the algebra structure).
IsAlgebraic.exists_nonzero_eq_adjoin_mul theorem
{s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) : ∃ᵉ (t ∈ Algebra.adjoin R { s }) (r ≠ (0 : R)), s * t = algebraMap R S r
Full source 
theorem IsAlgebraic.exists_nonzero_eq_adjoin_mul
    {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) :
    ∃ᵉ (t ∈ Algebra.adjoin R {s}) (r ≠ (0 : R)), s * t = algebraMap R S r := by
  have ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs
  have ⟨p, hp⟩ := X_dvd_sub_C (p := q)
  refine ⟨aeval s p, aeval_mem_adjoin_singleton _ _, _, neg_ne_zero.mpr hq0, ?_⟩
  apply_fun aeval s at hp
  rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp
Existence of Nonzero Element in Adjoint Algebra for Algebraic Non-Zero Divisors
Informal description
Let $R$ be a ring and $S$ an $R$-algebra. For any element $s \in S$ that is algebraic over $R$ and belongs to the non-zero divisors of $S$, there exists an element $t$ in the $R$-algebra generated by $s$ and a non-zero element $r \in R$ such that $s \cdot t$ equals the image of $r$ under the algebra map from $R$ to $S$.
IsAlgebraic.exists_nonzero_dvd theorem
{s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) : ∃ r : R, r ≠ 0 ∧ s ∣ algebraMap R S r
Full source 
theorem IsAlgebraic.exists_nonzero_dvd
    {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) :
    ∃ r : R, r ≠ 0 ∧ s ∣ algebraMap R S r := by
  obtain ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs
  have key := map_dvd (aeval s) (X_dvd_sub_C (p := q))
  rw [map_sub, hq, zero_sub, dvd_neg, aeval_X, aeval_C] at key
  exact ⟨q.coeff 0, hq0, key⟩
Existence of Nonzero Divisible Element for Algebraic Non-Zero Divisors
Informal description
Let $R$ be a ring and $S$ an $R$-algebra. For any element $s \in S$ that is algebraic over $R$ and belongs to the non-zero divisors of $S$, there exists a nonzero element $r \in R$ such that $s$ divides the image of $r$ under the algebra map from $R$ to $S$.
Algebra.IsAlgebraic.injective_tower_top theorem
(inj : Injective (algebraMap R A)) : Injective (algebraMap S A)
Full source 
theorem injective_tower_top (inj : Injective (algebraMap R A)) : Injective (algebraMap S A) := by
  refine (injective_iff_map_eq_zero _).mpr fun s eq ↦ of_not_not fun ne ↦ ?_
  have ⟨r, ne, dvd⟩ := (alg.1 s).exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero ne)
  refine ne (inj <| map_zero (algebraMap R A) ▸ zero_dvd_iff.mp ?_)
  simp_rw [← eq, IsScalarTower.algebraMap_apply R S A, map_dvd (algebraMap S A) dvd]
Injectivity of tower-top algebra map in algebraic extensions
Informal description
Let $R \to S \to A$ be a tower of algebra extensions where $A$ is algebraic over $R$. If the algebra map from $R$ to $A$ is injective, then the algebra map from $S$ to $A$ is also injective.
Algebra.IsAlgebraic.faithfulSMul_tower_top theorem
[FaithfulSMul R A] : FaithfulSMul S A
Full source 
theorem faithfulSMul_tower_top [FaithfulSMul R A] : FaithfulSMul S A := by
  rw [faithfulSMul_iff_algebraMap_injective] at *
  exact injective_tower_top S ‹_›
Faithfulness of scalar multiplication in algebraic tower extensions
Informal description
Let $R \to S \to A$ be a tower of algebra extensions where $A$ is algebraic over $R$. If the scalar multiplication action of $R$ on $A$ is faithful, then the scalar multiplication action of $S$ on $A$ is also faithful.
IsAlgebraic.exists_smul_eq_mul theorem
(a : S) {b : S} (hRb : IsAlgebraic R b) (hb : b ∈ nonZeroDivisors S) : ∃ᵉ (c : S) (d ≠ (0 : R)), d • a = b * c
Full source 
/-- A fraction `(a : S) / (b : S)` can be reduced to `(c : S) / (d : R)`,
if `b` is algebraic over `R`. -/
theorem IsAlgebraic.exists_smul_eq_mul
    (a : S) {b : S} (hRb : IsAlgebraic R b) (hb : b ∈ nonZeroDivisors S) :
    ∃ᵉ (c : S) (d ≠ (0 : R)), d • a = b * c :=
  have ⟨r, hr, s, h⟩ := hRb.exists_nonzero_dvd hb
  ⟨s * a, r, hr, by rw [Algebra.smul_def, h, mul_assoc]⟩
Existence of Scalar Multiplication Representation for Algebraic Non-Zero Divisors
Informal description
Let $R$ be a ring and $S$ an $R$-algebra. For any element $a \in S$ and any element $b \in S$ that is algebraic over $R$ and belongs to the non-zero divisors of $S$, there exist elements $c \in S$ and $d \in R$ with $d \neq 0$ such that $d \cdot a = b \cdot c$.
Algebra.IsAlgebraic.exists_smul_eq_mul theorem
[NoZeroDivisors S] [Algebra.IsAlgebraic R S] (a : S) {b : S} (hb : b ≠ 0) : ∃ᵉ (c : S) (d ≠ (0 : R)), d • a = b * c
Full source 
/-- A fraction `(a : S) / (b : S)` can be reduced to `(c : S) / (d : R)`,
if `b` is algebraic over `R`. -/
theorem Algebra.IsAlgebraic.exists_smul_eq_mul [NoZeroDivisors S] [Algebra.IsAlgebraic R S]
    (a : S) {b : S} (hb : b ≠ 0) :
    ∃ᵉ (c : S) (d ≠ (0 : R)), d • a = b * c :=
  (isAlgebraic b).exists_smul_eq_mul a (mem_nonZeroDivisors_of_ne_zero hb)
Existence of Scalar Multiplication Representation in Algebraic Algebras without Zero Divisors
Informal description
Let $R$ be a ring and $S$ an $R$-algebra that is algebraic over $R$ and has no zero divisors. For any element $a \in S$ and any nonzero element $b \in S$, there exist elements $c \in S$ and $d \in R$ with $d \neq 0$ such that $d \cdot a = b \cdot c$.
inv_eq_of_aeval_divX_ne_zero theorem
{x : L} {p : K[X]} (aeval_ne : aeval x (divX p) ≠ 0) : x⁻¹ = aeval x (divX p) / (aeval x p - algebraMap _ _ (p.coeff 0))
Full source 
theorem inv_eq_of_aeval_divX_ne_zero {x : L} {p : K[X]} (aeval_ne : aevalaeval x (divX p) ≠ 0) :
    x⁻¹ = aeval x (divX p) / (aeval x p - algebraMap _ _ (p.coeff 0)) := by
  rw [inv_eq_iff_eq_inv, inv_div, eq_comm, div_eq_iff, sub_eq_iff_eq_add, mul_comm]
  conv_lhs => rw [← divX_mul_X_add p]
  · rw [map_add, map_mul, aeval_X, aeval_C]
  · exact aeval_ne
Inverse Formula for Field Elements via Polynomial Evaluation
Informal description
Let $L$ be a field extension of $K$, and let $x \in L$ be an element such that the evaluation of the polynomial $\text{divX}(p)$ at $x$ is nonzero, i.e., $\text{aeval}_x(\text{divX}(p)) \neq 0$. Then the inverse of $x$ is given by \[ x^{-1} = \frac{\text{aeval}_x(\text{divX}(p))}{\text{aeval}_x(p) - \text{algebraMap}_K^L(p_0)}, \] where $p_0$ is the constant term of the polynomial $p$.
inv_eq_of_root_of_coeff_zero_ne_zero theorem
{x : L} {p : K[X]} (aeval_eq : aeval x p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) : x⁻¹ = -(aeval x (divX p) / algebraMap _ _ (p.coeff 0))
Full source 
theorem inv_eq_of_root_of_coeff_zero_ne_zero {x : L} {p : K[X]} (aeval_eq : aeval x p = 0)
    (coeff_zero_ne : p.coeff 0 ≠ 0) : x⁻¹ = -(aeval x (divX p) / algebraMap _ _ (p.coeff 0)) := by
  convert inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
    (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1
  · rw [aeval_eq, zero_sub, div_neg]
  rw [RingHom.map_zero]
  convert aeval_eq
  conv_rhs => rw [← divX_mul_X_add p]
  rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]
Inverse Formula for Roots of Polynomials with Nonzero Constant Term
Informal description
Let $L$ be a field extension of $K$, and let $x \in L$ be a root of a polynomial $p \in K[X]$ (i.e., $\text{aeval}_x(p) = 0$) with nonzero constant term $p_0 \neq 0$. Then the inverse of $x$ is given by \[ x^{-1} = -\frac{\text{aeval}_x(\text{divX}(p))}{\text{algebraMap}_K^L(p_0)}. \]
Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero theorem
{x : A} {p : K[X]} (aeval_eq : aeval x p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) : (x⁻¹ : L) ∈ A
Full source 
theorem Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {x : A} {p : K[X]}
    (aeval_eq : aeval x p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) : (x⁻¹ : L) ∈ A := by
  suffices (x⁻¹ : L) = (-p.coeff 0)⁻¹ • aeval x (divX p) by
    rw [this]
    exact A.smul_mem (aeval x _).2 _
  have : aeval (x : L) p = 0 := by rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]
  -- Porting note: this was a long sequence of `rw`.
  rw [inv_eq_of_root_of_coeff_zero_ne_zero this coeff_zero_ne, div_eq_inv_mul, Algebra.smul_def]
  simp only [aeval_coe, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, coe_toSubsemiring,
    coe_algebraMap]
  rw [map_inv₀, map_neg, inv_neg, neg_mul]
Inverse of Algebraic Element with Nonzero Constant Term Belongs to Subalgebra
Informal description
Let $A$ be a subalgebra of a field extension $L$ over $K$, and let $x \in A$ be a root of a polynomial $p \in K[X]$ (i.e., $\text{aeval}_x(p) = 0$) with nonzero constant term $p_0 \neq 0$. Then the inverse of $x$ in $L$ belongs to $A$, i.e., $x^{-1} \in A$.
Subalgebra.inv_mem_of_algebraic theorem
{x : A} (hx : _root_.IsAlgebraic K (x : L)) : (x⁻¹ : L) ∈ A
Full source 
theorem Subalgebra.inv_mem_of_algebraic {x : A} (hx : _root_.IsAlgebraic K (x : L)) :
    (x⁻¹ : L) ∈ A := by
  obtain ⟨p, ne_zero, aeval_eq⟩ := hx
  rw [Subalgebra.aeval_coe, Subalgebra.coe_eq_zero] at aeval_eq
  revert ne_zero aeval_eq
  refine p.recOnHorner ?_ ?_ ?_
  · intro h
    contradiction
  · intro p a hp ha _ih _ne_zero aeval_eq
    refine A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq ?_
    rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]
  · intro p hp ih _ne_zero aeval_eq
    rw [map_mul, aeval_X, mul_eq_zero] at aeval_eq
    rcases aeval_eq with aeval_eq | x_eq
    · exact ih hp aeval_eq
    · rw [x_eq, Subalgebra.coe_zero, inv_zero]
      exact A.zero_mem
Inverse of Algebraic Element in Subalgebra
Informal description
Let $A$ be a subalgebra of a field extension $L$ over $K$. For any element $x \in A$ that is algebraic over $K$, the inverse $x^{-1}$ in $L$ belongs to $A$.
Subalgebra.isField_of_algebraic theorem
[Algebra.IsAlgebraic K L] : IsField A
Full source 
/-- In an algebraic extension L/K, an intermediate subalgebra is a field. -/
@[stacks 0BID]
theorem Subalgebra.isField_of_algebraic [Algebra.IsAlgebraic K L] : IsField A :=
  { show Nontrivial A by infer_instance, Subalgebra.toCommRing A with
    mul_inv_cancel := fun {a} ha =>
      ⟨⟨a⁻¹, A.inv_mem_of_algebraic (Algebra.IsAlgebraic.isAlgebraic (a : L))⟩,
        Subtype.ext (mul_inv_cancel₀ (mt (Subalgebra.coe_eq_zero _).mp ha))⟩ }
Intermediate Subalgebra in Algebraic Extension is a Field
Informal description
Let $K$ be a field and $L$ be an algebraic field extension of $K$. If $A$ is an intermediate subalgebra between $K$ and $L$, then $A$ is a field.
Algebra.Transcendental.infinite theorem
[Algebra.Transcendental R A] : Infinite A
Full source 
theorem Algebra.Transcendental.infinite [Algebra.Transcendental R A] : Infinite A :=
  have ⟨x, hx⟩ := ‹Algebra.Transcendental R A›
  hx.infinite
Transcendental Algebra Implies Infinite Type
Informal description
If an $R$-algebra $A$ is transcendental over $R$ (i.e., contains at least one element transcendental over $R$), then $A$ is infinite as a type.