pow_odd — Mathlib

English

The nth power of a quadratic character is itself when n is odd.

Русский

Квадратичный характер ^ n остаётся χ, если n нечётно.

LaTeX

$$χ^n = χ for odd n$$

Lean4

/-- The `n`th power of a quadratic character is itself, when `n` is odd. -/
theorem pow_odd {χ : MulChar R R'} (hχ : χ.IsQuadratic) {n : ℕ} (hn : Odd n) : χ ^ n = χ :=
  by
  obtain ⟨n, rfl⟩ := hn
  rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]

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