Theorems · Definition · number theory

RingOfIntegers.ZModXQuotSpanEquivQuotSpanPair

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

If p does not divide exponent θ and Q is a lift of a monic irreducible factor of minpoly ℤ θ modulo p, then (ℤ / pℤ)[X] / Q ≃+* 𝓞 K / (p, Q(θ)).

Defined in: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Cited by: 1 results in Mathlib
Foundations: Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field NumberField Fact

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites29

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
Finsetstatement · cited by 13,712
Fieldstatement and proof · cited by 7,404
Polynomialstatement and proof · cited by 5,681
Idealstatement · cited by 4,748
AlgHomstatement · cited by 3,236
Factstatement and proof · cited by 2,726
HasQuotient.Quotientstatement · cited by 2,301
Nat.Primestatement and proof · cited by 2,059
RingEquivstatement · cited by 1,147
ZModstatement and proof · cited by 1,024

Cited by1

Results whose statement or proof uses this declaration.

NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_applyproof · cited by 1