norm_zeta_sub_one_of_prime_ne_two

English

If p is prime and K is a cyclotomic extension, then the discriminant of zeta_p^k minus 1 equals a power of p times a unit.

Русский

Если p — простое и K — циклотомическое расширение, то дискриминант ζ^k − 1 равен степени p, умноженной на единицу.

LaTeX

$$$\operatorname{discr} (\zeta^{k} - 1) = u \cdot p^n$ for some unit u and n$$

Lean4

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

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