Theorems · Theorem · number theory

RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ}
  [inst_2 : Fact (Nat.Prime p)] (hp : ¬p ∣ RingOfIntegers.exponent θ) (Q : Polynomial ℤ),
  (RingOfIntegers.ZModXQuotSpanEquivQuotSpan hp)
      ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}))
        (Polynomial.map (Int.castRingHom (ZMod p)) Q)) =
    (Ideal.Quotient.mk (Ideal.span {↑p})) ((Polynomial.aeval θ) Q)

Defined in

Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldNumberFieldFact