norm_toInteger_pow_sub_one_of_prime_ne_two

English

For isCyclotomic extension with order p^(k+1), the norm of (ζ^{p^s} − 1) equals p^{p^s} when s ≤ k and p ≠ 2.

Русский

Пусть порядок циклотомического расширения p^(k+1); тогда норма (ζ^{p^s} − 1) равна p^{p^s} для s ≤ k и p ≠ 2.

LaTeX

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

Lean4

/-- The norm, relative to `ℤ`, of `ζ ^ p ^ s - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ`
is `p ^ p ^ s` if `s ≤ k` and `p ≠ 2`. -/
theorem norm_toInteger_pow_sub_one_of_prime_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : ℕ} (hs : s ≤ k) (hodd : p ≠ 2) :
    Algebra.norm ℤ (hζ.toInteger ^ p ^ s - 1) = p ^ p ^ s :=
  by
  refine hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two hs (fun h ↦ hodd ?_)
  apply eq_of_prime_pow_eq hp.out.prime Nat.prime_two.prime (k - s).succ_pos
  rwa [pow_one]

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