quadraticChar_dichotomy — Mathlib

English

For a nonzero element a in a finite field, the quadratic character takes values ±1.

Русский

Для ненулевого элемента a в конечном поле квадратичный характер принимает значения ±1.

LaTeX

$${a: F} (ha: a ≠ 0) → quadraticChar F a ∈ {1, -1}$$

Lean4

/-- The quadratic character is `1` or `-1` on nonzero arguments. -/
theorem quadraticChar_dichotomy {a : F} (ha : a ≠ 0) : quadraticChar F a = 1 ∨ quadraticChar F a = -1 :=
  sq_eq_one_iff.1 <| quadraticChar_sq_one ha

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