Theorems · Theorem · number theory

NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span

∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [inst_2 : NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ) {Q : Polynomial ℤ}
  (hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p),
  ↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) =
    Ideal.span {↑p, (Polynomial.aeval θ) Q}

The ideal corresponding to the class of Q ∈ ℤ[X] modulo p via NumberField.Ideal.primesOverSpanEquivMonicFactorsMod is spanned by p and Q(θ).

Defined in

Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFactNumberField