quadraticChar_eq_neg_one_iff_not_one

English

Let F be a finite field and a a nonzero element of F. Then the quadratic character χF(a) is either 1 or −1, i.e., χF(a) = −1 if and only if χF(a) ≠ 1.

Русский

Пусть F — конечное поле и a ∈ F не равен 0. Тогда квадратичный характер χF(a) равен либо 1, либо −1, то есть χF(a) = −1 тогда и только тогда, когда χF(a) ≠ 1.

LaTeX

$$$\forall F\ (\text{Field }F)\ (a\in F^{\times}),\quad \chi_F(a) = -1 \iff \chi_F(a) \neq 1$$$

Lean4

/-- The quadratic character is `1` or `-1` on nonzero arguments. -/
theorem quadraticChar_eq_neg_one_iff_not_one {a : F} (ha : a ≠ 0) : quadraticChar F a = -1 ↔ ¬quadraticChar F a = 1 :=
  ⟨fun h ↦ by rw [h]; cutsat, fun h₂ ↦ (or_iff_right h₂).mp (quadraticChar_dichotomy ha)⟩

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