English
If a fixed prime p does not divide exponent θ, then the natural isomorphism between the polynomial ring modulo the minimal polynomial of θ over Z/pZ and the quotient ring 𝓞K modulo p is established.
Русский
Если p не делит exponent(θ), существует естественное изоморфизм между полиномиальным кольцом по модулю минимального многочлена θ и факторкольцом 𝓞K/ p.
LaTeX
$$$(\\mathbb{Z}/p\\mathbb{Z})[X] / (\\minpoly_{\\mathbb{Z}}(\\theta)) \\cong \\mathcal{O}_K / (p).$$$
Lean4
theorem not_dvd_exponent_iff {p : ℕ} [Fact (Nat.Prime p)] :
¬p ∣ exponent θ ↔ Codisjoint (comap (algebraMap ℤ (𝓞 K)) (conductor ℤ θ)) (span {↑p}) :=
by
rw [codisjoint_comm, ← IsCoatom.not_le_iff_codisjoint, ← under_def, ← Ideal.dvd_iff_le, ←
Int.ideal_span_absNorm_eq_self (under ℤ (conductor ℤ θ)), span_singleton_dvd_span_singleton_iff_dvd,
Int.natCast_dvd_natCast, exponent]
exact isMaximal_def.mp <| Int.ideal_span_isMaximal_of_prime p
