norm_eq_one_of_linearly_ordered — Mathlib

English

If K is a linearly ordered field and ζ is a primitive root of order n with n odd, then the norm N_{L/K}(ζ) equals 1.

Русский

Пусть K — линейно упорядоченное поле, и ζ — примитивный корень порядка n, где n нечётно; тогда N_{L/K}(ζ) = 1.

LaTeX

$$$\operatorname{Norm}_{L/K}(\zeta) = 1$$$

Lean4

/-- If `K` is linearly ordered, the norm of a primitive root is `1` if `n` is odd. -/
theorem norm_eq_one_of_linearly_ordered {K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Algebra K L]
    (hodd : Odd n) : norm K ζ = 1 :=
  by
  have hz := congr_arg (norm K) ((IsPrimitiveRoot.iff_def _ n).1 hζ).1
  rw [← (algebraMap K L).map_one, Algebra.norm_algebraMap, one_pow, map_pow, ← one_pow n] at hz
  exact StrictMono.injective hodd.strictMono_pow hz

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