ringOfIntegers — Mathlib

English

If IsCyclotomicExtension {2^k} K L and k ≥ 2, then the norm of zeta(2^k)^ (2^s) − 1 equals 2^ (2^s).

Русский

Если IsCyclotomicExtension {2^k} K L и k ≥ 2, то норма zeta(2^k)^{2^s} − 1 равна 2^{2^s}.

LaTeX

$$$\operatorname{Norm}_{K}(\zeta^{2^s} - 1) = 2^{2^s}$$$

Lean4

/-- The ring of integers of a `p ^ k`-th cyclotomic extension of `ℚ` is a cyclotomic extension. -/
instance ringOfIntegers [IsCyclotomicExtension {p ^ k} ℚ K] : IsCyclotomicExtension {p ^ k} ℤ (𝓞 K) :=
  let _ := (zeta_spec (p ^ k) ℚ K).adjoin_isCyclotomicExtension ℤ
  IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec (p ^ k) ℚ K).adjoinEquivRingOfIntegers

Похожие утверждения