Theorems · Definition · number theory

RingOfIntegers.ZModXQuotSpanEquivQuotSpan

{K : Type u_1} →
  [inst : Field K] →
    [NumberField K] →
      {θ : NumberField.RingOfIntegers K} →
        {p : ℕ} →
          [inst_2 : Fact (Nat.Prime p)] →
            ¬p ∣ RingOfIntegers.exponent θ →
              Polynomial (ZMod p) ⧸ Ideal.span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ≃+*
                NumberField.RingOfIntegers K ⧸ Ideal.span {↑p}

If p doesn't divide the exponent of θ, then (ℤ / pℤ)[X] / (minpoly θ) ≃+* 𝓞 K / p(𝓞 K).

Defined in

Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldNumberFieldFact