∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F],
  ringChar F ≠ 2 →
    ∀ {p : ℕ} [inst_2 : Fact (Nat.Prime p)],
      p ≠ 2 → (IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(ZMod.χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1)