norm_zeta_pow_sub_one_of_prime_ne_two

English

There exist u ∈ Z^× and n ∈ N such that the discriminant of the ζ − 1 power basis equals u · p^n.

Русский

Существуют u ∈ Z^× и n ∈ N такие, что дискриминант базиса ζ − 1 равен u · p^n.

LaTeX

$$$\exists u \in \mathbb{Z}^{\times}, \exists n \in \mathbb{N},\; \operatorname{discr} = u \cdot p^n$$$

Lean4

/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is an odd
prime, then the norm of `zeta (p ^ (k + 1)) K L - 1` is `p`. -/
theorem norm_zeta_pow_sub_one_of_prime_ne_two {k : ℕ} [Fact p.Prime] [IsCyclotomicExtension {p ^ (k + 1)} K L]
    (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) (h : p ≠ 2) : norm K (zeta (p ^ (k + 1)) K L - 1) = p :=
  (zeta_spec _ K L).norm_sub_one_of_prime_ne_two hirr h

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