pow_even — Mathlib

English

The nth power of a quadratic character is trivial when n is even.

Русский

Степень n квадратичного характера равна единице, если n чётна.

LaTeX

$$If χ is quadratic and n is even, then χ^n = 1$$

Lean4

/-- The `n`th power of a quadratic character is the trivial character, when `n` is even. -/
theorem pow_even {χ : MulChar R R'} (hχ : χ.IsQuadratic) {n : ℕ} (hn : Even n) : χ ^ n = 1 :=
  by
  obtain ⟨n, rfl⟩ := even_iff_two_dvd.mp hn
  rw [pow_mul, hχ.sq_eq_one, one_pow]

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