English
The number of solutions to x^2 = a in F is χF(a) + 1.
Русский
Число решений уравнения x^2 = a в F равно χF(a) + 1.
LaTeX
$$$\#\{x\in F : x^2 = a\} = χ_F(a) + 1$$$
Lean4
/-- The number of solutions to `x^2 = a` is determined by the quadratic character. -/
theorem quadraticChar_card_sqrts (hF : ringChar F ≠ 2) (a : F) :
#{x : F | x ^ 2 = a}.toFinset = quadraticChar F a + 1 := by
-- we consider the cases `a = 0`, `a` is a nonzero square and `a` is a nonsquare in turn
by_cases h₀ : a = 0
·
simp only [h₀, sq_eq_zero_iff, Set.setOf_eq_eq_singleton, Set.toFinset_card, Set.card_singleton, Int.natCast_succ,
Int.ofNat_zero, MulChar.map_zero]
· set s := {x : F | x ^ 2 = a}.toFinset
by_cases h : IsSquare a
· rw [(quadraticChar_one_iff_isSquare h₀).mpr h]
rcases h with ⟨b, h⟩
rw [h, mul_self_eq_zero] at h₀
have h₁ : s = [b, -b].toFinset := by
ext1
rw [← pow_two] at h
simp_rw [s, Set.toFinset_setOf, mem_filter_univ, h, List.toFinset_cons, List.toFinset_nil, insert_empty_eq,
mem_insert, mem_singleton]
exact sq_eq_sq_iff_eq_or_eq_neg
norm_cast
rw [h₁, List.toFinset_cons, List.toFinset_cons, List.toFinset_nil]
exact card_pair (Ne.symm (mt (Ring.eq_self_iff_eq_zero_of_char_ne_two hF).mp h₀))
· rw [quadraticChar_neg_one_iff_not_isSquare.mpr h]
simp only [neg_add_cancel, Int.natCast_eq_zero, card_eq_zero, eq_empty_iff_forall_notMem]
simpa [s, isSquare_iff_exists_sq, eq_comm] using h
