Theorems · Theorem · number theory
FiniteField.isSquare_two_iff
∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F], IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 52 is a square in F iff #F is not congruent to 3 or 5 mod 8.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 221 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- 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
- ZMod.χ₈_nat_eq_if_mod_eightproof · cited by 3
- FiniteField.even_card_of_char_twoproof · cited by 3
- quadraticChar_twoproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- ZMod.exists_sq_eq_two_iffproof · cited by 1