English
If p does not divide the exponent of θ, then the prime ideals of 𝓞_K lying over the ideal (p) correspond bijectively to the monic irreducible factors of minpoly_ℤ(θ) modulo p.
Русский
Если p не делит показатель θ, то простые идеалы над (p) в 𝓞_K устанавливают биекцию с моничными иррод факторами минимального полинома θ по модулю p.
LaTeX
$$$\text{primesOver}(\operatorname{span}\{p\}) (\mathcal{O}_K) \cong \text{monicFactorsMod}(\theta, p),$ с условием $p \nmid \mathrm{exponent}(\theta)$.$$
Lean4
/-- 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`.
-/
def primesOverSpanEquivMonicFactorsMod (hp : ¬p ∣ exponent θ) :
primesOver (span {(p : ℤ)}) (𝓞 K) ≃ monicFactorsMod θ p :=
have h : span {(p : ℤ)} ≠ ⊥ := by simp [NeZero.ne p]
((Equiv.setCongr (by ext; simp [mem_primesOver_iff_mem_normalizedFactors _ h])).trans
(normalizedFactorsMapEquivNormalizedFactorsMinPolyMk (Int.ideal_span_isMaximal_of_prime p) h
(not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral)).trans <|
(primesOverSpanEquivMonicFactorsModAux _)
