norm_eq_neg_one_pow — Mathlib

English

Let ζ be a primitive 2nd root of unity in a cyclotomic extension; then the field norm of ζ from L to K equals (−1) raised to the degree [L:K].

Русский

Пусть ζ — примитивный корень единицы порядка 2 в циклотомическом расширении; тогда нормa поля N_{L/K}(ζ) равна (−1)^{[L:K]}.

LaTeX

$$$\operatorname{Norm}_{L/K}(\zeta) = (-1)^{\operatorname{finrank}_K L}$$$

Lean4

/-- This mathematically trivial result is complementary to `norm_eq_one` below. -/
theorem norm_eq_neg_one_pow (hζ : IsPrimitiveRoot ζ 2) [IsDomain L] : norm K ζ = (-1 : K) ^ finrank K L := by
  rw [hζ.eq_neg_one_of_two_right, show -1 = algebraMap K L (-1) by simp, Algebra.norm_algebraMap]

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