pow_char — Mathlib

English

If χ is quadratic and p is prime with R' of characteristic p, then the p-th power of χ is χ itself: χ^p = χ.

Русский

Если χ квадратичный, p — простое число, и характеристика кольца R' равна p, то χ^p = χ.

LaTeX

$$$χ^p = χ$$$

Lean4

/-- The `p`th power of a quadratic character is itself, when `p` is the (prime) characteristic
of the target ring. -/
theorem pow_char {χ : MulChar R R'} (hχ : χ.IsQuadratic) (p : ℕ) [hp : Fact p.Prime] [CharP R' p] : χ ^ p = χ :=
  by
  ext x
  rw [pow_apply_coe]
  rcases hχ x with (hx | hx | hx) <;> rw [hx]
  · rw [zero_pow (@Fact.out p.Prime).ne_zero]
  · rw [one_pow]
  · exact neg_one_pow_char R' p

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