Theorems · Theorem · field theory
Fintype.nonempty_field_iff
∀ {α : Type u_1} [inst : Fintype α], Nonempty (Field α) ↔ IsPrimePow (Fintype.card α)A Fintype can be given a field structure iff its cardinality is a prime power.
- Defined in
- Mathlib.FieldTheory.Cardinality
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 159 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
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
- Equiv.symmproof · cited by 3,681
- Factproof · cited by 2,726
- Nat.Primeproof · cited by 2,059
- LT.lt.ne'proof · cited by 1,417
- Fintype.cardstatement and proof · cited by 1,386
- Primeproof · cited by 277
- Fintype.ofFiniteproof · cited by 255
- IsPrimePowstatement and proof · cited by 77
- Fintype.card_eq_nat_cardproof · cited by 31
- Fintype.equivOfCardEqproof · cited by 23
Cited by2
Results whose statement or proof uses this declaration.
- Field.nonempty_iffproof · cited by 0
- Fintype.not_isField_of_card_not_prime_powproof · cited by 0