norm_of_cyclotomic_irreducible — Mathlib

English

Let n be a natural number, ζ a primitive n-th root in a cyclotomic extension, and cyclotomic_n K irreducible. Then the norm of ζ from K to the base field equals 1 if n ≠ 2 and equals −1 if n = 2.

Русский

Пусть n — натуральное число, ζ — примитивный корень n-ой степени в циклотомическом расширении, и cyclotomic_n K ирреducible. Тогда норма ζ равна 1, если n ≠ 2, и −1, если n = 2.

LaTeX

$$$\operatorname{Norm}_{K}(\zeta) = \begin{cases} 1, & n \neq 2 \\ -1, & n = 2 \end{cases}$$$

Lean4

theorem norm_of_cyclotomic_irreducible [IsDomain L] [IsCyclotomicExtension { n } K L]
    (hirr : Irreducible (cyclotomic n K)) : norm K ζ = ite (n = 2) (-1) 1 :=
  by
  split_ifs with hn
  · subst hn
    rw [norm_eq_neg_one_pow (K := K) hζ, IsCyclotomicExtension.finrank _ hirr]
    norm_cast
  · exact hζ.norm_eq_one hn hirr

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