# Adjoining roots of polynomials #

This file defines the commutative ring AdjoinRoot f, the ring R[X]/(f) obtained from a commutative ring R and a polynomial f : R[X]. If furthermore R is a field and f is irreducible, the field structure on AdjoinRoot f is constructed.

We suggest stating results on IsAdjoinRoot instead of AdjoinRoot to achieve higher generality, since IsAdjoinRoot works for all different constructions of R[α] including AdjoinRoot f = R[X]/(f) itself.

## Main definitions and results #

The main definitions are in the AdjoinRoot namespace.

• mk f : R[X] →+* AdjoinRoot f, the natural ring homomorphism.

• of f : R →+* AdjoinRoot f, the natural ring homomorphism.

• root f : AdjoinRoot f, the image of X in R[X]/(f).

• lift (i : R →+* S) (x : S) (h : f.eval₂ i x = 0) : (AdjoinRoot f) →+* S, the ring homomorphism from R[X]/(f) to S extending i : R →+* S and sending X to x.

• lift_hom (x : S) (hfx : aeval x f = 0) : AdjoinRoot f →ₐ[R] S, the algebra homomorphism from R[X]/(f) to S extending algebraMap R S and sending X to x

• equiv : (AdjoinRoot f →ₐ[F] E) ≃ {x // x ∈ f.aroots E} a bijection between algebra homomorphisms from AdjoinRoot and roots of f in S

def AdjoinRoot {R : Type u} [] (f : ) :

Adjoin a root of a polynomial f to a commutative ring R. We define the new ring as the quotient of R[X] by the principal ideal generated by f.

Equations
Instances For
instance AdjoinRoot.instCommRing {R : Type u} [] (f : ) :
Equations
instance AdjoinRoot.instInhabited {R : Type u} [] (f : ) :
Equations
• = { default := 0 }
instance AdjoinRoot.instDecidableEq {R : Type u} [] (f : ) :
Equations
theorem AdjoinRoot.nontrivial {R : Type u} [] (f : ) [] (h : f.degree 0) :
def AdjoinRoot.mk {R : Type u} [] (f : ) :

Ring homomorphism from R[x] to AdjoinRoot f sending X to the root.

Equations
Instances For
theorem AdjoinRoot.induction_on {R : Type u} [] (f : ) {C : } (x : ) (ih : ∀ (p : ), C (() p)) :
C x
def AdjoinRoot.of {R : Type u} [] (f : ) :

Embedding of the original ring R into AdjoinRoot f.

Equations
• = ().comp Polynomial.C
Instances For
instance AdjoinRoot.instSMulAdjoinRoot {R : Type u} {S : Type v} [] (f : ) [] [] :
SMul S ()
Equations
instance AdjoinRoot.instDistribSMulOfIsScalarTower {R : Type u} {S : Type v} [] (f : ) [] [] :
Equations
@[simp]
theorem AdjoinRoot.smul_mk {R : Type u} {S : Type v} [] (f : ) [] [] (a : S) (x : ) :
a () x = () (a x)
theorem AdjoinRoot.smul_of {R : Type u} {S : Type v} [] (f : ) [] [] (a : S) (x : R) :
a () x = () (a x)
instance AdjoinRoot.instIsScalarTower {R : Type u} [] (R₁ : Type u_1) (R₂ : Type u_2) [SMul R₁ R₂] [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R] [IsScalarTower R₂ R R] [IsScalarTower R₁ R₂ R] (f : ) :
IsScalarTower R₁ R₂ ()
Equations
• =
instance AdjoinRoot.instSMulCommClass {R : Type u} [] (R₁ : Type u_1) (R₂ : Type u_2) [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R] [IsScalarTower R₂ R R] [SMulCommClass R₁ R₂ R] (f : ) :
SMulCommClass R₁ R₂ ()
Equations
• =
instance AdjoinRoot.isScalarTower_right {R : Type u} {S : Type v} [] (f : ) [] [] :
Equations
• =
instance AdjoinRoot.instDistribMulActionOfIsScalarTower {R : Type u} {S : Type v} [] [] [] [] (f : ) :
Equations
instance AdjoinRoot.instAlgebra {R : Type u} {S : Type v} [] (f : ) [] [Algebra S R] :
Algebra S ()
Equations
@[simp]
theorem AdjoinRoot.algebraMap_eq {R : Type u} [] (f : ) :
theorem AdjoinRoot.algebraMap_eq' {R : Type u} (S : Type v) [] (f : ) [] [Algebra S R] :
algebraMap S () = ().comp ()
theorem AdjoinRoot.finiteType {R : Type u} [] (f : ) :
theorem AdjoinRoot.finitePresentation {R : Type u} [] (f : ) :
def AdjoinRoot.root {R : Type u} [] (f : ) :

Equations
• = () Polynomial.X
Instances For
instance AdjoinRoot.hasCoeT {R : Type u} [] {f : } :
CoeTC R ()
Equations
• AdjoinRoot.hasCoeT = { coe := () }
theorem AdjoinRoot.algHom_ext {R : Type u} {S : Type v} [] {f : } [] [Algebra R S] {g₁ : →ₐ[R] S} {g₂ : →ₐ[R] S} (h : g₁ () = g₂ ()) :
g₁ = g₂

Two R-AlgHom from AdjoinRoot f to the same R-algebra are the same iff they agree on root f.

@[simp]
theorem AdjoinRoot.mk_eq_mk {R : Type u} [] {f : } {g : } {h : } :
() g = () h f g - h
@[simp]
theorem AdjoinRoot.mk_eq_zero {R : Type u} [] {f : } {g : } :
() g = 0 f g
@[simp]
theorem AdjoinRoot.mk_self {R : Type u} [] {f : } :
() f = 0
@[simp]
theorem AdjoinRoot.mk_C {R : Type u} [] {f : } (x : R) :
() (Polynomial.C x) = () x
@[simp]
theorem AdjoinRoot.mk_X {R : Type u} [] {f : } :
() Polynomial.X =
theorem AdjoinRoot.mk_ne_zero_of_degree_lt {R : Type u} [] {f : } (hf : f.Monic) {g : } (h0 : g 0) (hd : g.degree < f.degree) :
() g 0
theorem AdjoinRoot.mk_ne_zero_of_natDegree_lt {R : Type u} [] {f : } (hf : f.Monic) {g : } (h0 : g 0) (hd : g.natDegree < f.natDegree) :
() g 0
@[simp]
theorem AdjoinRoot.aeval_eq {R : Type u} [] {f : } (p : ) :
p = () p
@[simp]
theorem AdjoinRoot.eval₂_root {R : Type u} [] (f : ) :
= 0
theorem AdjoinRoot.isRoot_root {R : Type u} [] (f : ) :
().IsRoot ()
theorem AdjoinRoot.isAlgebraic_root {R : Type u} [] {f : } (hf : f 0) :
theorem AdjoinRoot.of.injective_of_degree_ne_zero {R : Type u} [] {f : } [] (hf : f.degree 0) :
def AdjoinRoot.lift {R : Type u} {S : Type v} [] {f : } [] (i : R →+* S) (x : S) (h : = 0) :

Lift a ring homomorphism i : R →+* S to AdjoinRoot f →+* S.

Equations
Instances For
@[simp]
theorem AdjoinRoot.lift_mk {R : Type u} {S : Type v} [] {f : } [] {i : R →+* S} {a : S} (h : = 0) (g : ) :
() (() g) =
@[simp]
theorem AdjoinRoot.lift_root {R : Type u} {S : Type v} [] {f : } [] {i : R →+* S} {a : S} (h : = 0) :
() () = a
@[simp]
theorem AdjoinRoot.lift_of {R : Type u} {S : Type v} [] {f : } [] {i : R →+* S} {a : S} (h : = 0) {x : R} :
() (() x) = i x
@[simp]
theorem AdjoinRoot.lift_comp_of {R : Type u} {S : Type v} [] {f : } [] {i : R →+* S} {a : S} (h : = 0) :
().comp () = i
def AdjoinRoot.liftHom {R : Type u} {S : Type v} [] (f : ) [] [Algebra R S] (x : S) (hfx : () f = 0) :

Produce an algebra homomorphism AdjoinRoot f →ₐ[R] S sending root f to a root of f in S.

Equations
Instances For
@[simp]
theorem AdjoinRoot.coe_liftHom {R : Type u} {S : Type v} [] (f : ) [] [Algebra R S] (x : S) (hfx : () f = 0) :
@[simp]
theorem AdjoinRoot.aeval_algHom_eq_zero {R : Type u} {S : Type v} [] (f : ) [] [Algebra R S] (ϕ : →ₐ[R] S) :
(Polynomial.aeval (ϕ ())) f = 0
@[simp]
theorem AdjoinRoot.liftHom_eq_algHom {R : Type u} {S : Type v} [] [] [Algebra R S] (f : ) (ϕ : →ₐ[R] S) :
AdjoinRoot.liftHom f (ϕ ()) = ϕ
@[simp]
theorem AdjoinRoot.liftHom_mk {R : Type u} {S : Type v} [] (f : ) [] {a : S} [Algebra R S] (hfx : () f = 0) {g : } :
(AdjoinRoot.liftHom f a hfx) (() g) = () g
@[simp]
theorem AdjoinRoot.liftHom_root {R : Type u} {S : Type v} [] (f : ) [] {a : S} [Algebra R S] (hfx : () f = 0) :
(AdjoinRoot.liftHom f a hfx) () = a
@[simp]
theorem AdjoinRoot.liftHom_of {R : Type u} {S : Type v} [] (f : ) [] {a : S} [Algebra R S] (hfx : () f = 0) {x : R} :
(AdjoinRoot.liftHom f a hfx) (() x) = () x
@[simp]
theorem AdjoinRoot.root_isInv {R : Type u} [] (r : R) :
(AdjoinRoot.of (Polynomial.C r * Polynomial.X - 1)) r * AdjoinRoot.root (Polynomial.C r * Polynomial.X - 1) = 1
theorem AdjoinRoot.algHom_subsingleton {R : Type u} [] {S : Type u_1} [] [Algebra R S] {r : R} :
Subsingleton (AdjoinRoot (Polynomial.C r * Polynomial.X - 1) →ₐ[R] S)
theorem AdjoinRoot.isDomain_of_prime {R : Type u} [] {f : } (hf : ) :
theorem AdjoinRoot.noZeroSMulDivisors_of_prime_of_degree_ne_zero {R : Type u} [] {f : } [] (hf : ) (hf' : f.degree 0) :
instance AdjoinRoot.span_maximal_of_irreducible {K : Type w} [] {f : } [Fact ()] :
(Ideal.span {f}).IsMaximal
Equations
• =
noncomputable instance AdjoinRoot.instGroupWithZero {K : Type w} [] {f : } [Fact ()] :
Equations
noncomputable instance AdjoinRoot.instField {K : Type w} [] {f : } [Fact ()] :
Equations
• One or more equations did not get rendered due to their size.
theorem AdjoinRoot.coe_injective {K : Type w} [] {f : } (h : f.degree 0) :
theorem AdjoinRoot.coe_injective' {K : Type w} [] {f : } [Fact ()] :
theorem AdjoinRoot.mul_div_root_cancel {K : Type w} [] (f : ) [Fact ()] :
(Polynomial.X - Polynomial.C ()) * ( / (Polynomial.X - Polynomial.C ())) =
instance AdjoinRoot.instIsNoetherianRing {R : Type u} [] [] {f : } :
Equations
• =
theorem AdjoinRoot.isIntegral_root' {R : Type u} [] {g : } (hg : g.Monic) :
def AdjoinRoot.modByMonicHom {R : Type u} [] {g : } (hg : g.Monic) :

AdjoinRoot.modByMonicHom sends the equivalence class of f mod g to f %ₘ g.

This is a well-defined right inverse to AdjoinRoot.mk, see AdjoinRoot.mk_leftInverse.

Equations
• = ().liftQ g.modByMonicHom ∘ₗ .symm
Instances For
@[simp]
theorem AdjoinRoot.modByMonicHom_mk {R : Type u} [] {g : } (hg : g.Monic) (f : ) :
(() f) = f %ₘ g
theorem AdjoinRoot.mk_leftInverse {R : Type u} [] {g : } (hg : g.Monic) :
theorem AdjoinRoot.mk_surjective {R : Type u} [] {g : } :
def AdjoinRoot.powerBasisAux' {R : Type u} [] {g : } (hg : g.Monic) :
Basis (Fin g.natDegree) R ()

The elements 1, root g, ..., root g ^ (d - 1) form a basis for AdjoinRoot g, where g is a monic polynomial of degree d.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AdjoinRoot.powerBasisAux'_repr_symm_apply {R : Type u} [] {g : } (hg : g.Monic) (c : Fin g.natDegree →₀ R) :
.repr.symm c = () (i : Fin g.natDegree, () (c i))
@[simp]
theorem AdjoinRoot.powerBasisAux'_repr_apply_to_fun {R : Type u} [] {g : } (hg : g.Monic) (f : ) (i : Fin g.natDegree) :
(.repr f) i = ( f).coeff i
@[simp]
theorem AdjoinRoot.powerBasis'_gen {R : Type u} [] {g : } (hg : g.Monic) :
.gen =
@[simp]
theorem AdjoinRoot.powerBasis'_dim {R : Type u} [] {g : } (hg : g.Monic) :
.dim = g.natDegree
def AdjoinRoot.powerBasis' {R : Type u} [] {g : } (hg : g.Monic) :

The power basis 1, root g, ..., root g ^ (d - 1) for AdjoinRoot g, where g is a monic polynomial of degree d.

Equations
• = { gen := , dim := g.natDegree, basis := , basis_eq_pow := }
Instances For
theorem AdjoinRoot.isIntegral_root {K : Type w} [] {f : } (hf : f 0) :
theorem AdjoinRoot.minpoly_root {K : Type w} [] {f : } (hf : f 0) :
def AdjoinRoot.powerBasisAux {K : Type w} [] {f : } (hf : f 0) :
Basis (Fin f.natDegree) K ()

The elements 1, root f, ..., root f ^ (d - 1) form a basis for AdjoinRoot f, where f is an irreducible polynomial over a field of degree d.

Equations
• = let f' := f * Polynomial.C f.leadingCoeff⁻¹; let_fun deg_f' := ; let_fun minpoly_eq := ; Basis.mk
Instances For
@[simp]
theorem AdjoinRoot.powerBasis_gen {K : Type w} [] {f : } (hf : f 0) :
.gen =
@[simp]
theorem AdjoinRoot.powerBasis_dim {K : Type w} [] {f : } (hf : f 0) :
.dim = f.natDegree
def AdjoinRoot.powerBasis {K : Type w} [] {f : } (hf : f 0) :

The power basis 1, root f, ..., root f ^ (d - 1) for AdjoinRoot f, where f is an irreducible polynomial over a field of degree d.

Equations
• = { gen := , dim := f.natDegree, basis := , basis_eq_pow := }
Instances For
theorem AdjoinRoot.minpoly_powerBasis_gen {K : Type w} [] {f : } (hf : f 0) :
minpoly K .gen = f * Polynomial.C f.leadingCoeff⁻¹
theorem AdjoinRoot.minpoly_powerBasis_gen_of_monic {K : Type w} [] {f : } (hf : f.Monic) (hf' : optParam (f 0) ) :
minpoly K ().gen = f
@[simp]
theorem AdjoinRoot.Minpoly.toAdjoin_apply (R : Type u) {S : Type v} [] [] [Algebra R S] (x : S) :
∀ (a : ), a = (QuotientAddGroup.lift () (Polynomial.eval₂RingHom (algebraMap R (Algebra.adjoin R {x})) x, ) ) a
def AdjoinRoot.Minpoly.toAdjoin (R : Type u) {S : Type v} [] [] [Algebra R S] (x : S) :

The surjective algebra morphism R[X]/(minpoly R x) → R[x]. If R is a integrally closed domain and x is integral, this is an isomorphism, see minpoly.equivAdjoin.

Equations
Instances For
theorem AdjoinRoot.Minpoly.toAdjoin_apply' {R : Type u} {S : Type v} [] [] [Algebra R S] {x : S} (a : AdjoinRoot (minpoly R x)) :
a = (AdjoinRoot.liftHom (minpoly R x) x, ) a
theorem AdjoinRoot.Minpoly.toAdjoin.apply_X {R : Type u} {S : Type v} [] [] [Algebra R S] {x : S} :
((AdjoinRoot.mk (minpoly R x)) Polynomial.X) = x,
theorem AdjoinRoot.Minpoly.toAdjoin.surjective (R : Type u) {S : Type v} [] [] [Algebra R S] (x : S) :
@[simp]
theorem AdjoinRoot.equiv'_apply {R : Type u} {S : Type v} [] [] [Algebra R S] (g : ) (pb : ) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
@[simp]
theorem AdjoinRoot.equiv'_symm_apply {R : Type u} {S : Type v} [] [] [Algebra R S] (g : ) (pb : ) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
(AdjoinRoot.equiv' g pb h₁ h₂).symm = (pb.lift () h₁)
def AdjoinRoot.equiv' {R : Type u} {S : Type v} [] [] [Algebra R S] (g : ) (pb : ) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :

If S is an extension of R with power basis pb and g is a monic polynomial over R such that pb.gen has a minimal polynomial g, then S is isomorphic to AdjoinRoot g.

Compare PowerBasis.equivOfRoot, which would require h₂ : aeval pb.gen (minpoly R (root g)) = 0; that minimal polynomial is not guaranteed to be identical to g.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AdjoinRoot.equiv'_toAlgHom {R : Type u} {S : Type v} [] [] [Algebra R S] (g : ) (pb : ) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
theorem AdjoinRoot.equiv'_symm_toAlgHom {R : Type u} {S : Type v} [] [] [Algebra R S] (g : ) (pb : ) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (Polynomial.aeval pb.gen) g = 0) :
(AdjoinRoot.equiv' g pb h₁ h₂).symm = pb.lift () h₁
def AdjoinRoot.equiv (L : Type u_1) (F : Type u_2) [] [] [] [Algebra F L] (f : ) (hf : f 0) :
( →ₐ[F] L) { x : L // x f.aroots L }

If L is a field extension of F and f is a polynomial over F then the set of maps from F[x]/(f) into L is in bijection with the set of roots of f in L.

Equations
Instances For
def AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk {R : Type u} [] (I : ) (f : ) :
≃+* Ideal.map () (Ideal.map Polynomial.C I)

The natural isomorphism R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f)) for α a root of f : R[X] and I : Ideal R.

See adjoin_root.quot_map_of_equiv for the isomorphism with (R/I)[X] / (f mod I).

Equations
Instances For
@[simp]
theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk {R : Type u} [] (I : ) (f : ) (x : ) :
(() x) = (Ideal.Quotient.mk (Ideal.map () (Ideal.map Polynomial.C I))) x
theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk {R : Type u} [] (I : ) (f : ) (x : ) :
.symm ((Ideal.Quotient.mk (Ideal.map () (Ideal.map Polynomial.C I))) x) = () x
def AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk {R : Type u} [] (I : ) (f : ) :
Ideal.map () (Ideal.map Polynomial.C I) ≃+* ( Ideal.map Polynomial.C I) Ideal.map (Ideal.Quotient.mk (Ideal.map Polynomial.C I)) (Ideal.span {f})

The natural isomorphism R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x]) for α a root of f : R[X] and I : Ideal R

Equations
Instances For
theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk {R : Type u} [] (I : ) (f : ) (p : ) :
((Ideal.Quotient.mk (Ideal.map () (Ideal.map Polynomial.C I))) (() p)) = (DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p
@[simp]
theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk {R : Type u} [] (I : ) (f : ) (p : ) :
((DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p) = (Ideal.Quotient.mk (Ideal.map () (Ideal.map Polynomial.C I))) (() p)
def AdjoinRoot.Polynomial.quotQuotEquivComm {R : Type u} [] (I : ) (f : ) :
Polynomial (R I) ≃+* ( Ideal.map Polynomial.C I) Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f}

The natural isomorphism (R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x]) where f : R[X] and I : Ideal R

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AdjoinRoot.Polynomial.quotQuotEquivComm_mk {R : Type u} [] (I : ) (f : ) (p : ) :
(() ()) = (Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f})) ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) p)
@[simp]
theorem AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk {R : Type u} [] (I : ) (f : ) (p : ) :
.symm ((Ideal.Quotient.mk (Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f})) ((Ideal.Quotient.mk (Ideal.map Polynomial.C I)) p)) = () ()

The natural isomorphism R[α]/I[α] ≅ (R/I)[X]/(f mod I) for α a root of f : R[X] and I : Ideal R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of {R : Type u} [] (I : ) (f : ) (p : ) :
(() (() p)) = () ()
@[simp]
theorem AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk {R : Type u} [] (I : ) (f : ) (p : ) :
(() ()) = () (() p)
@[simp]
theorem AdjoinRoot.quotEquivQuotMap_symm_apply {R : Type u} [] (f : ) (I : ) (a : Polynomial (R I) ) :
.symm a = a
@[simp]
theorem AdjoinRoot.quotEquivQuotMap_apply {R : Type u} [] (f : ) (I : ) (a : ) :
noncomputable def AdjoinRoot.quotEquivQuotMap {R : Type u} [] (f : ) (I : ) :

Promote AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot to an alg_equiv.

Equations
Instances For
@[simp]
theorem AdjoinRoot.quotEquivQuotMap_apply_mk {R : Type u} [] (f : ) (g : ) (I : ) :
(() (() g)) = () ()
theorem AdjoinRoot.quotEquivQuotMap_symm_apply_mk {R : Type u} [] (f : ) (g : ) (I : ) :
.symm (() ()) = () (() g)
@[simp]
theorem PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply {R : Type u} {S : Type v} [] [] [Algebra R S] (pb : ) (I : ) :
∀ (a : Polynomial (R I) Ideal.span {Polynomial.map (minpoly R pb.gen)}), (pb.quotientEquivQuotientMinpolyMap I).symm a = ().symm (((AdjoinRoot.quotEquivQuotMap (minpoly R pb.gen) I)).symm a)
@[simp]
theorem PowerBasis.quotientEquivQuotientMinpolyMap_apply {R : Type u} {S : Type v} [] [] [Algebra R S] (pb : ) (I : ) :
∀ (a : S Ideal.map () I), (pb.quotientEquivQuotientMinpolyMap I) a = () ((Ideal.quotientMap (Ideal.map (AdjoinRoot.of (minpoly R pb.gen)) I) ((AdjoinRoot.equiv' (minpoly R pb.gen) pb )).symm ) a)
noncomputable def PowerBasis.quotientEquivQuotientMinpolyMap {R : Type u} {S : Type v} [] [] [Algebra R S] (pb : ) (I : ) :

Let α have minimal polynomial f over R and I be an ideal of R, then R[α] / (I) = (R[x] / (f)) / pS = (R/p)[x] / (f mod p).

Equations
Instances For
theorem PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk {R : Type u} {S : Type v} [] [] [Algebra R S] (pb : ) (I : ) (g : ) :
(pb.quotientEquivQuotientMinpolyMap I) ((Ideal.Quotient.mk (Ideal.map () I)) ((Polynomial.aeval pb.gen) g)) = (Ideal.Quotient.mk (Ideal.span {Polynomial.map (minpoly R pb.gen)})) ()
theorem PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk {R : Type u} {S : Type v} [] [] [Algebra R S] (pb : ) (I : ) (g : ) :
(pb.quotientEquivQuotientMinpolyMap I).symm ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (minpoly R pb.gen)})) ()) = (Ideal.Quotient.mk (Ideal.map () I)) ((Polynomial.aeval pb.gen) g)
theorem Irreducible.exists_dvd_monic_irreducible_of_isIntegral {K : Type u_1} {L : Type u_2} [] [] [] [Algebra K L] [] {f : } (hf : ) :
∃ (g : ), g.Monic f Polynomial.map () g

If L / K is an integral extension, K is a domain, L is a field, then any irreducible polynomial over L divides some monic irreducible polynomial over K.