quadraticChar_isQuadratic — Mathlib

English

The quadratic character χF is quadratic as a multiplicative character.

Русский

Квадратичный характер χF является квадратичным по отношению к умножению.

LaTeX

$$$\chi_F\text{ is quadratic as a multiplicative character}$$$

Lean4

/-- The quadratic character is quadratic as a multiplicative character. -/
theorem quadraticChar_isQuadratic : (quadraticChar F).IsQuadratic :=
  by
  intro a
  by_cases ha : a = 0
  · left; rw [ha]; exact quadraticChar_zero
  · right; exact quadraticChar_dichotomy ha

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