@[simp]

theorem Polynomial.aeval_apply_X {A : Type u_1} {B : Type u_2} [CommSemiring A] [Semiring B] [Algebra A B] (φ : Polynomial A →ₐ[A] B) : aeval (φ X) = φ

theorem Polynomial.eq_of_ideal_span_eq_of_monic {R : Type u_1} [CommSemiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (h : Ideal.span {p} = Ideal.span {q}) : p = q

theorem RingHom.subsingleton {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} : f 1 = 0 ↔ Subsingleton S

theorem RingHom.ker_eq_top_iff {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} : ker f = ⊤ ↔ Subsingleton S

theorem RingHom.subsingleton_of_ker_eq_top {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} : ker f = ⊤ → Subsingleton S

Alias of the forward direction of RingHom.ker_eq_top_iff.

theorem RingHom.ker_eq_top_of_subsingleton' {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [Subsingleton S] {f : R →+* S} : ker f = ⊤

noncomputable def Polynomial.AlgHomEquiv (A : Type u_1) (B : Type u_2) [CommSemiring A] [Semiring B] [Algebra A B] : B ≃ (Polynomial A →ₐ[A] B)

Equations

• Polynomial.AlgHomEquiv A B = { toFun := fun (y : B) => Polynomial.aeval y, invFun := fun (f : Polynomial A →ₐ[A] B) => f Polynomial.X, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Polynomial.AlgHomEquiv_apply (A : Type u_1) (B : Type u_2) [CommSemiring A] [Semiring B] [Algebra A B] (y : B) : (AlgHomEquiv A B) y = aeval y

@[simp]

theorem Polynomial.AlgHomEquiv_symm_apply (A : Type u_1) (B : Type u_2) [CommSemiring A] [Semiring B] [Algebra A B] (f : Polynomial A →ₐ[A] B) : (AlgHomEquiv A B).symm f = f X

noncomputable def MvPolynomial.AlgHomEquiv (A : Type u_1) (B : Type u_2) (σ : Type u_3) [CommSemiring A] [CommSemiring B] [Algebra A B] : (σ → B) ≃ (MvPolynomial σ A →ₐ[A] B)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MvPolynomial.AlgHomEquiv_apply (A : Type u_1) (B : Type u_2) (σ : Type u_3) [CommSemiring A] [CommSemiring B] [Algebra A B] (y : σ → B) : (AlgHomEquiv A B σ) y = aeval y

@[simp]

theorem MvPolynomial.AlgHomEquiv_symm_apply (A : Type u_1) (B : Type u_2) (σ : Type u_3) [CommSemiring A] [CommSemiring B] [Algebra A B] (f : MvPolynomial σ A →ₐ[A] B) (i : σ) : (AlgHomEquiv A B σ).symm f i = f (X i)

structure Algebra.IsGenerator (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) : Prop

• adjoin_eq_top : R[x] = ⊤

theorem Algebra.IsGenerator.def (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) : IsGenerator R x ↔ R[x] = ⊤

theorem Algebra.isGenerator_iff_aeval_surjective (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) : IsGenerator R x ↔ Function.Surjective ⇑(Polynomial.aeval x)

theorem Algebra.IsGenerator.aeval_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) : Function.Surjective ⇑(Polynomial.aeval x)

noncomputable def Algebra.IsGenerator.adjoinEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) : ↥R[x] ≃ₐ[R] S

Equations

• hx.adjoinEquiv = (R[x].equivOfEq ⊤ ⋯).trans Subalgebra.topEquiv

theorem Algebra.IsGenerator.adjoinEquiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) (y : ↥R[x]) : hx.adjoinEquiv y = ↑y

theorem Algebra.IsGenerator.adjoinEquiv_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) (y : S) : ↑(hx.adjoinEquiv.symm y) = y

theorem Algebra.IsGenerator.finite_iff_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) : Module.Finite R S ↔ IsIntegral R x

theorem Algebra.IsGenerator.of_root_mem_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {y : S} (hy : x ∈ R[y]) : IsGenerator R y

theorem Algebra.IsGenerator.add_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) (r : R) : IsGenerator R (x + (algebraMap R S) r)

theorem Algebra.IsGenerator.algebraMap_mul {S : Type u_2} [Ring S] {F : Type u_3} [Field F] [Algebra F S] {x : S} (hx : IsGenerator F x) {r : F} (hr : r ≠ 0) : IsGenerator F ((algebraMap F S) r * x)

noncomputable def Algebra.IsGenerator.liftEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] : { y : T // ∀ (g : Polynomial R), (Polynomial.aeval x) g = 0 → (Polynomial.aeval y) g = 0 } ≃ (S →ₐ[R] T)

Equations

• hx.liftEquiv = ((Polynomial.AlgHomEquiv R T).subtypeEquiv ⋯).trans ((Polynomial.aeval x).liftOfSurjective' ⋯)

@[simp]

theorem Algebra.IsGenerator.liftEquiv_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] (φ : S →ₐ[R] T) : ↑(hx.liftEquiv.symm φ) = φ x

theorem Algebra.IsGenerator.algHom_ext {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] ⦃φ ψ : S →ₐ[R] T⦄ (h : φ x = ψ x) : φ = ψ

@[simp]

theorem Algebra.IsGenerator.liftEquiv_aeval_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : ∀ (g : Polynomial R), (Polynomial.aeval x) g = 0 → (Polynomial.aeval y) g = 0) (g : Polynomial R) : (hx.liftEquiv ⟨y, hy⟩) ((Polynomial.aeval x) g) = (Polynomial.aeval y) g

@[simp]

theorem Algebra.IsGenerator.liftEquiv_comp_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : ∀ (g : Polynomial R), (Polynomial.aeval x) g = 0 → (Polynomial.aeval y) g = 0) : (hx.liftEquiv ⟨y, hy⟩).comp (Polynomial.aeval x) = Polynomial.aeval y

@[simp]

theorem Algebra.IsGenerator.liftEquiv_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsGenerator R x) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : ∀ (g : Polynomial R), (Polynomial.aeval x) g = 0 → (Polynomial.aeval y) g = 0) : (hx.liftEquiv ⟨y, hy⟩) x = y

theorem Algebra.isUnit_iff_subsingleton_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) : IsUnit g ↔ Subsingleton S

theorem Algebra.subsingleton_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) : IsUnit g → Subsingleton S

Alias of the forward direction of Algebra.isUnit_iff_subsingleton_of_ker_aeval.

theorem Algebra.isUnit_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [Subsingleton S] (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) : IsUnit g

theorem Algebra.nontrivial_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) (hg : ¬IsUnit g) : Nontrivial S

theorem Algebra.not_isUnit_of_ker_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [Nontrivial S] (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) : ¬IsUnit g

theorem Algebra.aeval_eq_zero_iff_of_ker_aeval_eq_span_singleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) {f : Polynomial R} : (Polynomial.aeval x) f = 0 ↔ g ∣ f

structure Algebra.IsSimpleGenerator {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) extends Algebra.IsGenerator R x : Prop

• adjoin_eq_top : R[x] = ⊤
• ker_aeval : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}

theorem Algebra.IsSimpleGenerator.def {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) : IsSimpleGenerator x g ↔ IsGenerator R x ∧ RingHom.ker (Polynomial.aeval x) = Ideal.span {g}

theorem Algebra.IsSimpleGenerator.aeval_eq_zero_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {f : Polynomial R} : (Polynomial.aeval x) f = 0 ↔ g ∣ f

theorem Algebra.IsSimpleGenerator.aeval_self {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) : (Polynomial.aeval x) g = 0

theorem Algebra.IsSimpleGenerator.aeval_gen_eq_zero_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} {T : Type u_3} [Ring T] [Algebra R T] (y : T) (h : IsSimpleGenerator x g) : (Polynomial.aeval y) g = 0 ↔ ∀ (f : Polynomial R), (Polynomial.aeval x) f = 0 → (Polynomial.aeval y) f = 0

noncomputable def Algebra.IsSimpleGenerator.liftEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] : { y : T // (Polynomial.aeval y) g = 0 } ≃ (S →ₐ[R] T)

Equations

• h.liftEquiv = ((Equiv.refl T).subtypeEquiv ⋯).trans ⋯.liftEquiv

@[simp]

theorem Algebra.IsSimpleGenerator.liftEquiv_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] {φ : S →ₐ[R] T} : ↑(h.liftEquiv.symm φ) = φ x

noncomputable def Algebra.IsSimpleGenerator.lift {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) g = 0) : S →ₐ[R] T

Equations

• h.lift hy = h.liftEquiv ⟨y, hy⟩

@[simp]

theorem Algebra.IsSimpleGenerator.lift_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) g = 0) (f : Polynomial R) : (h.lift hy) ((Polynomial.aeval x) f) = (Polynomial.aeval y) f

@[simp]

theorem Algebra.IsSimpleGenerator.lift_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) g = 0) : (h.lift hy) x = y

@[simp]

theorem Algebra.IsSimpleGenerator.liftEquiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) g = 0) (h : IsSimpleGenerator x g) {z : S} : (h.liftEquiv ⟨y, hy⟩) z = (h.lift hy) z

noncomputable def Algebra.IsSimpleGenerator.equivOfRoot {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) : S ≃ₐ[R] S'

Equations

• h.equivOfRoot h' hx hx' = AlgEquiv.ofAlgHom (h.lift hx') (h'.lift hx) ⋯ ⋯

theorem Algebra.IsSimpleGenerator.equivOfRoot_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) (a : S) : (h.equivOfRoot h' hx hx') a = (h.lift hx') a

@[simp]

theorem Algebra.IsSimpleGenerator.equivOfRoot_symm {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) : (h.equivOfRoot h' hx hx').symm = h'.equivOfRoot h hx' hx

@[simp]

theorem Algebra.IsSimpleGenerator.equivOfRoot_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) (f : Polynomial R) : (h.equivOfRoot h' hx hx') ((Polynomial.aeval x) f) = (Polynomial.aeval x') f

@[simp]

theorem Algebra.IsSimpleGenerator.equivOfRoot_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} {g' : Polynomial R} (h' : IsSimpleGenerator x' g') (hx : (Polynomial.aeval x) g' = 0) (hx' : (Polynomial.aeval x') g = 0) : (h.equivOfRoot h' hx hx') x = x'

noncomputable def Algebra.IsSimpleGenerator.equiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsSimpleGenerator x' g) : S ≃ₐ[R] S'

Equations

• h.equiv h' = h.equivOfRoot h' ⋯ ⋯

@[simp]

theorem Algebra.IsSimpleGenerator.equiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsSimpleGenerator x' g) (z : S) : (h.equiv h') z = (h.equivOfRoot h' ⋯ ⋯) z

@[simp]

theorem Algebra.IsSimpleGenerator.equiv_symm {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {S' : Type u_4} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsSimpleGenerator x' g) : (h.equiv h').symm = h'.equiv h

theorem Algebra.IsSimpleGenerator.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} {T : Type u_4} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) (h : IsSimpleGenerator x g) : IsSimpleGenerator (φ x) g

@[simp]

theorem Algebra.IsSimpleGenerator.equivOfRoot_map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsSimpleGenerator x g) {T : Type u_4} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) : h.equivOfRoot ⋯ ⋯ ⋯ = φ

structure IsIntegralUnique {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) : Prop

• monic : g.Monic
• ker_aeval : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}

theorem IsIntegralUnique.of_subsingleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) [Subsingleton R] : IsIntegralUnique x g

theorem IsIntegralUnique.of_subsingleton_gen_one (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) [Subsingleton S] : IsIntegralUnique x 1

theorem IsIntegralUnique.of_ker_aeval_eq_span_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsIntegral R x) (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {minpoly R x}) : IsIntegralUnique x (minpoly R x)

theorem IsIntegralUnique.of_ker_aeval_eq_span' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [IsDomain R] (hx : IsIntegral R x) (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) : have hu := ⋯; IsIntegralUnique x (Polynomial.C ↑hu.unit⁻¹ * g)

theorem IsIntegralUnique.of_ker_aeval_eq_span {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [IsDomain R] [NormalizationMonoid R] (hx : IsIntegral R x) (h : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}) : IsIntegralUnique x (normalize g)

theorem IsIntegralUnique.of_aeval_eq_zero_imp_minpoly_dvd {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsIntegral R x) (h : ∀ {f : Polynomial R}, (Polynomial.aeval x) f = 0 → minpoly R x ∣ f) : IsIntegralUnique x (minpoly R x)

theorem IsIntegralUnique.of_unique_of_degree_le_degree_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsIntegral R x) (h : ∀ (f : Polynomial R), f.Monic → (Polynomial.aeval x) f = 0 → f.degree ≤ (minpoly R x).degree → f = minpoly R x) : IsIntegralUnique x (minpoly R x)

theorem IsIntegralUnique.aeval_eq_zero_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {f : Polynomial R} : (Polynomial.aeval x) f = 0 ↔ g ∣ f

theorem IsIntegralUnique.aeval_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) : (Polynomial.aeval x) g = 0

theorem IsIntegralUnique.isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) : IsIntegral R x

theorem IsIntegralUnique.gen_eq_one_iff_subsingleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) : g = 1 ↔ Subsingleton S

theorem IsIntegralUnique.subsingleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) : g = 1 → Subsingleton S

Alias of the forward direction of IsIntegralUnique.gen_eq_one_iff_subsingleton.

theorem IsIntegralUnique.gen_eq_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [Subsingleton S] (h : IsIntegralUnique x g) : g = 1

theorem IsIntegralUnique.nontrivial {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) (hg : g ≠ 1) : Nontrivial S

theorem IsIntegralUnique.gen_ne_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [Nontrivial S] (h : IsIntegralUnique x g) : g ≠ 1

theorem IsIntegralUnique.natDegree_gen_pos {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [Nontrivial S] (h : IsIntegralUnique x g) : 0 < g.natDegree

theorem IsIntegralUnique.degree_gen_pos {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [Nontrivial S] (h : IsIntegralUnique x g) : 0 < g.degree

theorem IsIntegralUnique.minpoly_eq_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) : minpoly R x = g

theorem IsIntegralUnique.gen_unique {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {g' : Polynomial R} (h' : IsIntegralUnique x g') : g = g'

theorem IsIntegralUnique.irreducible_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} [IsDomain R] [IsDomain S] (h : IsIntegralUnique x g) : Irreducible g

theorem IsIntegralUnique.isIntegralUnique_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) : IsIntegralUnique x (minpoly R x)

theorem IsIntegralUnique.eq_gen_of_degree_le_degree_gen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {f : Polynomial R} (hmo : f.Monic) (hf : (Polynomial.aeval x) f = 0) (fmin : f.degree ≤ g.degree) : f = g

theorem IsIntegralUnique.eq_gen_of_aeval_eq_zero_imp_degree_ge {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {f : Polynomial R} (hmo : f.Monic) (hf : (Polynomial.aeval x) f = 0) (hmin : ∀ (k : Polynomial R), k.Monic → (Polynomial.aeval x) k = 0 → f.degree ≤ k.degree) : f = g

theorem IsIntegralUnique.eq_gen_of_ker_aeval_eq_span {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) {f : Polynomial R} (hf : f.Monic) (hker : RingHom.ker (Polynomial.aeval x) = Ideal.span {f}) : f = g

theorem IsIntegralUnique.modByMonic_gen_eq_iff_aeval_eq {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUnique x g) (f₁ f₂ : Polynomial R) : f₁ %ₘ g = f₂ %ₘ g ↔ (Polynomial.aeval x) f₁ = (Polynomial.aeval x) f₂

structure IsIntegralUniqueGen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) (g : Polynomial R) extends Algebra.IsSimpleGenerator x g, IsIntegralUnique x g : Prop

• adjoin_eq_top : R[x] = ⊤
• ker_aeval : RingHom.ker (Polynomial.aeval x) = Ideal.span {g}
• monic : g.Monic

theorem IsIntegralUniqueGen.isIntegralUniqueGen_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : IsIntegralUniqueGen x (minpoly R x)

theorem IsIntegralUniqueGen.of_basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} [Module.Finite R S] {n : ℕ} (B : Module.Basis (Fin n) R S) (hB : ∀ (i : Fin n), B i = x ^ ↑i) : IsIntegralUniqueGen x (Polynomial.X ^ n - ∑ i : Fin n, Polynomial.C ((B.repr (x ^ n)) i) * Polynomial.X ^ ↑i)

noncomputable def Module.Basis.mkOfSpanning {ι : Type u_3} {R : Type u_4} {M : Type u_5} [Fintype ι] [CommRing R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Free R M] {v : ι → M} (hι : Fintype.card ι = finrank R M) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) : Basis ι R M

Equations

• Module.Basis.mkOfSpanning hι hsp = Module.Basis.ofEquivFun (LinearEquiv.ofBijective ((Module.piEquiv ι R M) v) ⋯).symm

@[simp]

theorem Module.Basis.coe_mkOfSpanning {ι : Type u_3} {R : Type u_4} {M : Type u_5} [Fintype ι] [CommRing R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Free R M] {v : ι → M} (hι : Fintype.card ι = finrank R M) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) : ⇑(mkOfSpanning hι hsp) = v

theorem Submodule.span_range_natDegree_minpoly_eq_adjoin {R : Type u_3} {A : Type u_4} [CommRing R] [Ring A] [Algebra R A] {x : A} (hx : IsIntegral R x) : span R ↑(Finset.image (fun (x_1 : ℕ) => x ^ x_1) (Finset.range (minpoly R x).natDegree)) = Subalgebra.toSubmodule R[x]

theorem IsIntegralUniqueGen.of_free {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} [Module.Finite R S] [Module.Free R S] (hx : Algebra.IsGenerator R x) : IsIntegralUniqueGen x (minpoly R x)

noncomputable def IsIntegralUniqueGen.repr {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : S →ₗ[R] Polynomial R

Equations

• h.repr = { toFun := fun (y : S) => Classical.choose ⋯ %ₘ g, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem IsIntegralUniqueGen.aeval_repr {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (y : S) : (Polynomial.aeval x) (h.repr y) = y

@[simp]

theorem IsIntegralUniqueGen.repr_aeval {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (f : Polynomial R) : h.repr ((Polynomial.aeval x) f) = f %ₘ g

theorem IsIntegralUniqueGen.repr_aeval_eq_self_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial R] (f : Polynomial R) : h.repr ((Polynomial.aeval x) f) = f ↔ f.degree < g.degree

theorem IsIntegralUniqueGen.repr_aeval_eq_self {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {f : Polynomial R} (hf : f.degree < g.degree) : h.repr ((Polynomial.aeval x) f) = f

@[simp]

theorem IsIntegralUniqueGen.repr_root_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {n : ℕ} (hdeg : n < g.natDegree) : h.repr (x ^ n) = Polynomial.X ^ n

@[simp]

theorem IsIntegralUniqueGen.repr_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (hdeg : 1 < g.natDegree) : h.repr x = Polynomial.X

@[simp]

theorem IsIntegralUniqueGen.repr_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] : h.repr 1 = 1

@[simp]

theorem IsIntegralUniqueGen.repr_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (r : R) : h.repr ((algebraMap R S) r) = (algebraMap R (Polynomial R)) r

@[simp]

theorem IsIntegralUniqueGen.repr_ofNat {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (n : ℕ) [n.AtLeastTwo] : h.repr (OfNat.ofNat n) = ↑↑n

@[simp]

theorem IsIntegralUniqueGen.repr_root_pow_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : h.repr (x ^ g.natDegree) = Polynomial.X ^ g.natDegree - g

theorem IsIntegralUniqueGen.degree_repr_le {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial R] (y : S) : (h.repr y).degree < g.degree

theorem IsIntegralUniqueGen.natDegree_repr_le {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (y : S) : (h.repr y).natDegree < g.natDegree

theorem IsIntegralUniqueGen.repr_coeff_of_natDegree_le {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (y : S) {i : ℕ} (hi : g.natDegree ≤ i) : (h.repr y).coeff i = 0

noncomputable def IsIntegralUniqueGen.liftEquivAroots {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] : { y : T // y ∈ g.aroots T } ≃ (S →ₐ[R] T)

Equations

• h.liftEquivAroots = ((Equiv.refl T).subtypeEquiv ⋯).trans ⋯.liftEquiv

@[simp]

theorem IsIntegralUniqueGen.liftEquivAroots_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] (φ : S →ₐ[R] T) : ↑(h.liftEquivAroots.symm φ) = φ x

@[simp]

theorem IsIntegralUniqueGen.liftEquivAroots_apply_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] {y : T} (hy : y ∈ g.aroots T) (z : S) : (h.liftEquivAroots ⟨y, hy⟩) z = (⋯.lift ⋯) z

@[reducible, inline]

noncomputable abbrev IsIntegralUniqueGen.fintypeAlgHom {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] : Fintype (S →ₐ[R] T)

Equations

• h.fintypeAlgHom = Fintype.ofEquiv { y : T // y ∈ g.aroots T } h.liftEquivAroots

noncomputable def IsIntegralUniqueGen.equiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {S' : Type u_3} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsIntegralUniqueGen x' g) : S ≃ₐ[R] S'

Equations

• h.equiv h' = ⋯.equiv ⋯

@[simp]

theorem IsIntegralUniqueGen.equiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {S' : Type u_3} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsIntegralUniqueGen x' g) (z : S) : (h.equiv h') z = (⋯.equiv ⋯) z

@[simp]

theorem IsIntegralUniqueGen.equiv_symm {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {S' : Type u_3} [Ring S'] [Algebra R S'] {x' : S'} (h' : IsIntegralUniqueGen x' g) : (h.equiv h').symm = h'.equiv h

theorem IsIntegralUniqueGen.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} {T : Type u_3} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) (h : IsIntegralUniqueGen x g) : IsIntegralUniqueGen (φ x) g

@[simp]

theorem IsIntegralUniqueGen.equivOfRoot_map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {T : Type u_3} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) : ⋯.equivOfRoot ⋯ ⋯ ⋯ = φ

noncomputable def IsIntegralUniqueGen.coeff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : S →ₗ[R] ℕ →₀ R

Equations

• h.coeff = { toFun := Polynomial.coeff, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ h.repr

theorem IsIntegralUniqueGen.coeff_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (z : S) : h.coeff z = (h.repr z).coeff

theorem IsIntegralUniqueGen.coeff_apply_of_natDegree_le {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (z : S) {i : ℕ} (hi : g.natDegree ≤ i) : (h.coeff z) i = 0

theorem IsIntegralUniqueGen.coeff_root_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {n : ℕ} (hn : n < g.natDegree) : h.coeff (x ^ n) = Finsupp.single n 1

theorem IsIntegralUniqueGen.coeff_root_pow_natDegree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {i : ℕ} (hi : i < g.natDegree) : (h.coeff (x ^ g.natDegree)) i = -g.coeff i

theorem IsIntegralUniqueGen.coeff_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (hdeg : 1 < g.natDegree) : h.coeff x = Finsupp.single 1 1

@[simp]

theorem IsIntegralUniqueGen.coeff_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] : h.coeff 1 = Finsupp.single 0 1

@[simp]

theorem IsIntegralUniqueGen.coeff_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (r : R) : h.coeff ((algebraMap R S) r) = Finsupp.single 0 r

@[simp]

theorem IsIntegralUniqueGen.coeff_ofNat {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] (n : ℕ) [n.AtLeastTwo] : h.coeff (OfNat.ofNat n) = Finsupp.single 0 ↑n

@[simp]

theorem IsIntegralUniqueGen.Polynomial.coeff_toFinsupp {R : Type u_3} [Semiring R] (p : Polynomial R) : p.toFinsupp.coeff = p.coeff

noncomputable def IsIntegralUniqueGen.basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : Module.Basis (Fin g.natDegree) R S

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsIntegralUniqueGen.coe_basis {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : ⇑h.basis = fun (i : Fin g.natDegree) => x ^ ↑i

theorem IsIntegralUniqueGen.basis_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (i : Fin g.natDegree) : h.basis i = x ^ ↑i

theorem IsIntegralUniqueGen.root_pow_eq_basis_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {i : ℕ} (hdeg : i < g.natDegree) : x ^ i = h.basis ⟨i, hdeg⟩

theorem IsIntegralUniqueGen.root_eq_basis_one {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (hdeg : 1 < g.natDegree) : x = h.basis ⟨1, hdeg⟩

theorem IsIntegralUniqueGen.one_eq_basis_zero {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial S] : 1 = h.basis ⟨0, ⋯⟩

theorem IsIntegralUniqueGen.free {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : Module.Free R S

theorem IsIntegralUniqueGen.finite {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : Module.Finite R S

theorem IsIntegralUniqueGen.finrank_eq_natDegree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial R] : Module.finrank R S = g.natDegree

theorem IsIntegralUniqueGen.finrank_eq_degree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) [Nontrivial R] : ↑(Module.finrank R S) = g.degree

theorem IsIntegralUniqueGen.leftMulMatrix {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : (Algebra.leftMulMatrix h.basis) x = Matrix.of fun (i j : Fin g.natDegree) => if ↑j + 1 = g.natDegree then -g.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

theorem IsIntegralUniqueGen.basis_repr_eq_coeff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (y : S) (i : Fin g.natDegree) : (h.basis.repr y) i = (h.coeff y) ↑i

theorem IsIntegralUniqueGen.coeff_eq_basis_repr_of_lt_natDegree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (z : S) (i : ℕ) (hi : i < g.natDegree) : (h.coeff z) i = (h.basis.repr z) ⟨i, hi⟩

theorem IsIntegralUniqueGen.coeff_eq_basis_repr {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) (z : S) (i : ℕ) : (h.coeff z) i = if hi : i < g.natDegree then (h.basis.repr z) ⟨i, hi⟩ else 0

theorem IsIntegralUniqueGen.ext_elem {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) ⦃y z : S⦄ (hyz : ∀ i < g.natDegree, (h.coeff y) i = (h.coeff z) i) : y = z

theorem IsIntegralUniqueGen.ext_elem_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) {y z : S} : y = z ↔ ∀ i < g.natDegree, (h.coeff y) i = (h.coeff z) i

theorem IsIntegralUniqueGen.coeff_injective {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (h : IsIntegralUniqueGen x g) : Function.Injective ⇑h.coeff

structure IsAdjoinRoot' {R : Type u_1} (S : Type u_2) [CommRing R] [Ring S] [Algebra R S] (f : Polynomial R) : Prop

• exists_root : ∃ (x : S), Algebra.IsSimpleGenerator x f

noncomputable def IsAdjoinRoot'.root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) : S

Equations

• h.root = ⋯.choose

theorem IsAdjoinRoot'.pe {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) : Algebra.IsSimpleGenerator h.root f

noncomputable def IsAdjoinRoot'.liftEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) {T : Type u_3} [Ring T] [Algebra R T] : { y : T // (Polynomial.aeval y) f = 0 } ≃ (S →ₐ[R] T)

Equations

• h.liftEquiv = ((Equiv.refl T).subtypeEquiv ⋯).trans ⋯.liftEquiv

noncomputable def IsAdjoinRoot'.lift {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) {T : Type u_3} [Ring T] [Algebra R T] {y : T} (hy : (Polynomial.aeval y) f = 0) : S →ₐ[R] T

Equations

• h.lift hy = ⋯.lift hy

noncomputable def IsAdjoinRoot'.equiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) {T : Type u_3} [Ring T] [Algebra R T] (h' : IsAdjoinRoot' T f) : S ≃ₐ[R] T

Equations

• h.equiv h' = ⋯.equiv ⋯

theorem IsAdjoinRoot'.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRoot' S f) {T : Type u_3} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) : IsAdjoinRoot' T f

structure IsAdjoinRootMonic' {R : Type u_1} (S : Type u_2) [CommRing R] [Ring S] [Algebra R S] (f : Polynomial R) extends IsAdjoinRoot' S f : Prop

• exists_root : ∃ (x : S), Algebra.IsSimpleGenerator x f
• f_monic : f.Monic

theorem IsAdjoinRootMonic'.ofIsIntegralUniqueGen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} {x : S} (hx : IsIntegralUniqueGen x f) : IsAdjoinRootMonic' S f

theorem IsAdjoinRootMonic'.pe {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) : IsIntegralUniqueGen ⋯.root f

@[simp]

theorem IsAdjoinRootMonic'.minpoly_root {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) : minpoly R ⋯.root = f

theorem IsAdjoinRootMonic'.irreducible {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) [IsDomain R] [IsDomain S] : Irreducible f

theorem IsAdjoinRootMonic'.subsingleton {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) (hf : f = 1) : Subsingleton S

theorem IsAdjoinRootMonic'.nontrivial {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) (hf : f ≠ 1) : Nontrivial S

noncomputable def IsAdjoinRootMonic'.liftEquivAroots {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] : { y : T // y ∈ f.aroots T } ≃ (S →ₐ[R] T)

Equations

• h.liftEquivAroots = ⋯.liftEquivAroots

@[reducible]

noncomputable def IsAdjoinRootMonic'.fintypeAlgHom {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) {T : Type u_3} [CommRing T] [IsDomain T] [Algebra R T] : Fintype (S →ₐ[R] T)

Equations

• h.fintypeAlgHom = ⋯.fintypeAlgHom

theorem IsAdjoinRootMonic'.map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) {T : Type u_3} [Ring T] [Algebra R T] (φ : S ≃ₐ[R] T) : IsAdjoinRootMonic' T f

theorem IsAdjoinRootMonic'.free {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) : Module.Free R S

theorem IsAdjoinRootMonic'.finite {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) : Module.Finite R S

theorem IsAdjoinRootMonic'.finrank_eq_natDegree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) [Nontrivial R] : Module.finrank R S = f.natDegree

theorem IsAdjoinRootMonic'.finrank_eq_degree {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {f : Polynomial R} (h : IsAdjoinRootMonic' S f) [Nontrivial R] : ↑(Module.finrank R S) = f.degree