norm_toInteger_sub_one_of_prime_ne_two

English

If p is odd and ζ is a primitive p^(k+1)-th root, then the norm of (ζ^{p^s} − 1) equals p.

Русский

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

LaTeX

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

Lean4

/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ` is
`p` if `p ≠ 2`. -/
theorem norm_toInteger_sub_one_of_prime_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p ≠ 2) : Algebra.norm ℤ (hζ.toInteger - 1) = p := by
  simpa only [pow_zero, pow_one] using hζ.norm_toInteger_pow_sub_one_of_prime_ne_two (Nat.zero_le _) hodd

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