Theorems · Theorem · number theory
FiniteField.isSquare_neg_two_iff
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F], IsSquare (-2) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7-2 is a square in F iff #F is not congruent to 5 or 7 mod 8.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 222 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Fieldstatement and proof · cited by 7,404
- Fintype.cardstatement and proof · cited by 1,386
- IsSquarestatement · cited by 132
- ringCharproof · cited by 73
- neg_ne_zeroproof · cited by 70
- quadraticChar_one_iff_isSquareproof · cited by 6
- FiniteField.odd_card_of_char_ne_twoproof · cited by 6
- Ring.two_ne_zeroproof · cited by 5
- FiniteField.isSquare_of_char_twoproof · cited by 4
- FiniteField.even_card_of_char_twoproof · cited by 3
- quadraticChar_neg_twoproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- ZMod.exists_sq_eq_neg_two_iffproof · cited by 0