Theorem: symmetric_isSquare (ExponentialRamsey/Prereq/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean)

State before:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : Fintype.card F % 4 ≠ 3
x✝¹ x✝ : F
h : (fun x y => IsSquare (x - y)) x✝¹ x✝
⊢ (fun x y => IsSquare (x - y)) x✝ x✝¹
Tactic:
simpa using h.mul (FiniteField.isSquare_neg_one_iff.2 hF)
State after:
no goals