theorem Field.isIntegralUnique {R : Type u_1} {S : Type u_2} [Field R] [Ring S] [Algebra R S] {x : S} (h₁ : IsIntegral R x) : IsIntegralUnique x (minpoly R x)

theorem IsIntegrallyClosed.isIntegralUnique {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (h₁ : IsIntegral R x) : IsIntegralUnique x (minpoly R x)

theorem AdjoinRoot.isGenerator {R : Type u_1} [CommRing R] (f : Polynomial R) : Algebra.IsGenerator R (root f)

theorem AdjoinRoot.hasPrincipalKerAeval {R : Type u_1} [CommRing R] (f : Polynomial R) : Algebra.IsSimpleGenerator (root f) f

theorem AdjoinRoot.isIntegralUniqueGen {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) : IsIntegralUniqueGen (root f) f

theorem AdjoinRoot.isAdjoinRoot' {R : Type u_1} [CommRing R] (f : Polynomial R) : IsAdjoinRoot' (AdjoinRoot f) f

theorem AdjoinRoot.isAdjoinRootMonic' {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Monic) : IsAdjoinRootMonic' (AdjoinRoot f) f

@[simp]

theorem AdjoinRoot.finrank {R : Type u_1} [CommRing R] {f : Polynomial R} [Nontrivial R] (hf : f.Monic) : Module.finrank R (AdjoinRoot f) = f.natDegree

theorem AdjoinRoot.finite {R : Type u_1} [CommRing R] {f : Polynomial R} [Nontrivial R] (hf : f.Monic) : Module.Finite R (AdjoinRoot f)

theorem AdjoinRoot.free {R : Type u_1} [CommRing R] {f : Polynomial R} [Nontrivial R] (hf : f.Monic) : Module.Free R (AdjoinRoot f)

theorem Field.exists_isIntegralUniqueGen (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] : ∃ (x : E), IsIntegralUniqueGen x (minpoly F x)

theorem Field.exists_isAdjoinRootMonic (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] : ∃ (f : Polynomial F), IsAdjoinRootMonic' E f

theorem Algebra.adjoin.isIntegral (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Algebra.IsIntegral R S] (s : Set S) : Algebra.IsIntegral R ↥(adjoin R s)

@[simp]

theorem Algebra.adjoin.ker_aeval (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) : RingHom.ker (Polynomial.aeval ⟨x, ⋯⟩) = RingHom.ker (Polynomial.aeval x)

theorem Algebra.adjoin.aeval_minpoly (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) : (Polynomial.aeval ⟨x, ⋯⟩) (minpoly R x) = 0

theorem Algebra.adjoin.isIntegral_elem {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} (hx : IsIntegral R x) : IsIntegral R ⟨x, ⋯⟩

theorem Algebra.adjoin.isGenerator (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x : S) : IsGenerator R ⟨x, ⋯⟩

theorem Algebra.adjoin.hasPrincipalKerAeval {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}) : IsSimpleGenerator ⟨x, ⋯⟩ g

theorem Algebra.adjoin.isIntegralUnique {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (hx : IsIntegralUnique x g) : IsIntegralUnique ⟨x, ⋯⟩ g

theorem Algebra.adjoin.isIntegralUniqueGen {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {x : S} {g : Polynomial R} (hx : IsIntegralUnique x g) : IsIntegralUniqueGen ⟨x, ⋯⟩ g