Theorems · Definition · commutative algebra

PowerBasis.quotientEquivQuotientMinpolyMap

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (pb : PowerBasis R S) →
            (I : Ideal R) →
              (S ⧸ Ideal.map (algebraMap R S) I) ≃ₐ[R]
                Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}

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).

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

5 results in Mathlib

Foundations

Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra