English
If P is a nonzero prime ideal of 𝓞K and its absNorm is coprime to torsionOrder(K), then torsionOrder(K) divides absNorm(P) − 1.
Русский
Если P — непустой простой идеал 𝓞K и absNorm(P) взаимно простa с torsionOrder(K), то torsionOrder(K) делит absNorm(P) − 1.
LaTeX
$$$\\mathrm{torsionOrder}(K) \\mid (\\mathrm{absNorm}(P) - 1).$$$
Lean4
/-- If the norm of the (nonzero) prime ideal `P` is coprime with the order of the torsion of `K`, then
the norm of `P` is congruent to `1` modulo `torsionOrder K`.
-/
theorem torsionOrder_dvd_absNorm_sub_one {P : Ideal (𝓞 K)} (hP₀ : P ≠ ⊥) (hP₁ : P.IsPrime)
(hP₂ : (absNorm P).Coprime (torsionOrder K)) : torsionOrder K ∣ absNorm P - 1 :=
by
have : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hP₀ hP₁
let _ := Ideal.Quotient.field P
have hP₃ : absNorm P ≠ 1 := absNorm_eq_one_iff.not.mpr <| IsPrime.ne_top hP₁
have h := Subgroup.card_dvd_of_injective _ (torsionMapQuot_injective hP₃ hP₂)
rwa [Nat.card_eq_fintype_card, Nat.card_units] at h
