Theorems · Definition · number theory

NumberField.Ideal.primesOverSpanEquivMonicFactorsMod

{K : Type u_1} →
  [inst : Field K] →
    {θ : NumberField.RingOfIntegers K} →
      {p : ℕ} →
        [inst_1 : Fact (Nat.Prime p)] →
          [NumberField K] →
            ¬p ∣ RingOfIntegers.exponent θ →
              ↑((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)) ≃ ↥(RingOfIntegers.monicFactorsMod θ p)

If p does not divide exponent θ, then the prime ideals above p in K are in bijection with the monic irreducible factors of minpoly ℤ θ modulo p.

Defined in

Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Cited by

10 results in Mathlib

Foundations

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

Assumes

FieldFactNumberField