isQuadratic_χ₈' — Mathlib

English

Let χ8' be a Dirichlet character modulo 8 taking values in {0, 1, −1}. Then χ8' is a quadratic character (i.e., its values lie in {0,1,−1} and it is multiplicative).

Русский

Пусть χ8' — символ Дирихле по модулю 8, принимающий значения из {0, 1, −1}. Тогда χ8' является квадратичным символом (значения принадлежат {0,1,−1} и он мультипликативен).

LaTeX

$$$$\chi_8' : \mathbb{Z} \to \{0,1,-1\} \quad\land\quad \chi_8'(ab)=\chi_8'(a)\chi_8'(b).$$$$

Lean4

/-- `χ₈'` takes values in `{0, 1, -1}` -/
theorem isQuadratic_χ₈' : χ₈'.IsQuadratic := by
  unfold MulChar.IsQuadratic
  decide

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