Theorems · Theorem · logic and foundations
Finite.one_lt_card
∀ {α : Type u_1} [Finite α] [h : Nontrivial α], 1 < Nat.card α- Defined in
- Mathlib.SetTheory.Cardinal.NatCard
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FiniteNontrivial
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finitestatement and proof · cited by 3,029
- Nontrivialstatement and proof · cited by 2,416
- Nat.cardstatement · cited by 844
- Finite.one_lt_card_iff_nontrivialproof · cited by 11
Cited by12
Results whose statement or proof uses this declaration.
- FiniteField.finrank_extensionproof · cited by 3
- not_isAddCyclic_prod_of_infinite_nontrivialproof · cited by 2
- IsPGroup.bot_lt_centerproof · cited by 2
- FiniteField.unit_isSquare_iffproof · cited by 2
- IsPGroup.nontrivial_iff_cardproof · cited by 2
- alternatingGroup.isCyclic_of_card_le_threeproof · cited by 1
- Projectivization.card_of_finrankproof · cited by 1
- FiniteField.unitsMap_norm_surjectiveproof · cited by 1
- Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_Xproof · cited by 1
- ZMod.minOrderproof · cited by 1
- IsZGroup.commutator_ltproof · cited by 0
- Projectivization.card''proof · cited by 0