English
Same as above, but expressed in equality form for the field F in the codomain F.
Русский
То же самое, что и выше, выраженное через равенство в окружении поля F в коде.
LaTeX
$$$\text{If } \operatorname{ringChar}(F) \neq 2\text{ and } a \neq 0,\; χ_F(a) = \text{ite}\; (a^{|F|/2}=1)\; 1\; -1$$$
Lean4
theorem quadraticChar_eq_pow_of_char_ne_two' (hF : ringChar F ≠ 2) (a : F) :
(quadraticChar F a : F) = a ^ (Fintype.card F / 2) :=
by
by_cases ha : a = 0
· have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card two_pos
simp only [ha, quadraticChar_apply, quadraticCharFun_zero, Int.cast_zero, zero_pow this.ne']
· rw [quadraticChar_eq_pow_of_char_ne_two hF ha]
by_cases ha' : a ^ (Fintype.card F / 2) = 1
· simp only [ha', if_true, Int.cast_one]
· have ha'' := Or.resolve_left (FiniteField.pow_dichotomy hF ha) ha'
simp only [ha'', Int.cast_ite, Int.cast_one, Int.cast_neg, ite_eq_right_iff]
exact Eq.symm
