norm_toInteger_sub_one_of_prime_ne_two'

English

For p^(k+1)-th cyclotomic extension with p odd, the norm of (ζ^{p^s} − 1) equals p^{p^s}.

Русский

Для p^(k+1)-й циклотомы с нечетным p норма (ζ^{p^s} − 1) равна p^{p^s}.

LaTeX

$$$\\operatorname{norm}_{\\mathbb{Z}}\\bigl(h\\zeta^{p^{s}} - 1\\bigr) = p^{p^{s}}$$$

Lean4

/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p`-th cyclotomic extension of `ℚ` is `p` if
`p ≠ 2`. -/
theorem norm_toInteger_sub_one_of_prime_ne_two' [hcycl : IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p)
    (h : p ≠ 2) : Algebra.norm ℤ (hζ.toInteger - 1) = p :=
  by
  have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
  replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
  exact hζ.norm_toInteger_sub_one_of_prime_ne_two h

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