English
The norm from the number field to ℤ of ζ − 1 equals 1 when the cyclotomic extension is not a prime power.
Русский
Нормa из числа поля в ℤ для ζ − 1 равна 1, если расширение не является степенью простого числа.
LaTeX
$$$\\operatorname{norm}_{\\mathbb{Z}}(h\\zeta^{\\mathrm{toInteger}} - 1) = 1$$$
Lean4
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `n`-th cyclotomic extension of `ℚ` where `n` is not a
power of a prime number is `1`.
-/
theorem norm_toInteger_sub_one_eq_one {n : ℕ} [IsCyclotomicExtension { n } ℚ K] (hζ : IsPrimitiveRoot ζ n) (h₁ : 2 < n)
(h₂ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n) :
have : NeZero n := NeZero.of_gt h₁
norm ℤ (hζ.toInteger - 1) = 1 :=
by
have : NumberField K := IsCyclotomicExtension.numberField { n } ℚ K
have : NeZero n := NeZero.of_gt h₁
dsimp only
rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, map_one, RingOfIntegers.map_mk,
sub_one_norm_eq_eval_cyclotomic hζ h₁ (cyclotomic.irreducible_rat (NeZero.pos _)),
eval_one_cyclotomic_not_prime_pow h₂, Int.cast_one]
