English
If a nonzero prime ideal P has absNorm not equal to 1 and its absNorm is coprime to the torsion order of K, then absNorm(P) is congruent to 1 modulo torsionOrder(K).
Русский
Если P — непустой простый идеал, у которого absNorm не равен 1, и absNorm(P) и порядок torsion(K) взаимно просты, то absNorm(P) ≡ 1 (mod torsionOrder(K)).
LaTeX
$$$\\text{If } P \\text{ is nonzero prime with } (|\\mathrm{absNorm}(P)|, \\mathrm{torsionOrder}(K)) = 1, \\text{ then } \\mathrm{absNorm}(P) \\equiv 1 \\pmod{\\mathrm{torsionOrder}(K)}.$$$
Lean4
theorem not_coprime_norm_of_mk_eq_one [NumberField K] (hI : absNorm I ≠ 1) {n : ℕ} {ζ : K} (hn : 2 ≤ n)
(hζ : IsPrimitiveRoot ζ n)
(h :
let _ : NeZero n := NeZero.of_gt hn;
Ideal.Quotient.mk I hζ.toInteger = 1) :
¬(absNorm I).Coprime n := by
intro h₁
rw [← RingHom.map_one (Ideal.Quotient.mk I), Ideal.Quotient.eq] at h
obtain ⟨p, hp, h₂⟩ := Nat.exists_prime_and_dvd hI
have : Fact (p.Prime) := ⟨hp⟩
refine hp.not_dvd_one <| h₁ ▸ Nat.dvd_gcd h₂ ?_
exact
hζ.prime_dvd_of_dvd_norm_sub_one hn <| Int.dvd_trans (Int.natCast_dvd_natCast.mpr h₂) (absNorm_dvd_norm_of_mem h)
