Theorems · Definition · combinatorics
Fintype.card
(α : Type u_4) → [Fintype α] → ℕ
card α is the number of elements in α, defined when α is a fintype.
- Defined in
- Mathlib.Data.Fintype.Card
- Cited by
- 1,386 results in Mathlib
- Foundations
- Depth 13 from the axioms, rests on 51 definitions · uses propext
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- Finset.univproof · cited by 3,473
- Finset.cardproof · cited by 2,327
Cited by1,482
Results whose statement or proof uses this declaration.
- Fintype.card_finstatement · cited by 270
- Nat.card_eq_fintype_cardstatement · cited by 200
- Cardinal.mk_fintypestatement and proof · cited by 81
- Fintype.card_coestatement · cited by 72
- Fintype.card_congrstatement and proof · cited by 67
- Set.toFinset_cardstatement · cited by 63
- Fintype.card_congr'statement · cited by 60
- Fintype.card_uniquestatement · cited by 59
- Finset.card_univstatement · cited by 58
- Finset.densproof · cited by 55
- NumberField.InfinitePlace.nrComplexPlacesproof · cited by 52
- Fintype.equivFinstatement · cited by 51
Showing the 200 most cited of 1,482.