Theorems · Theorem · logic and foundations
ENat.card_eq_coe_fintype_card
∀ {α : Type u_1} [inst : Fintype α], ENat.card α = ↑(Fintype.card α)- Defined in
- Mathlib.SetTheory.Cardinal.Finite
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 89 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.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Fintypestatement and proof · cited by 7,736
- ENatstatement · cited by 4,985
- Fintype.cardstatement and proof · cited by 1,386
- map_natCastproof · cited by 134
- Cardinal.toENatproof · cited by 92
- ENat.cardstatement · cited by 89
- Cardinal.mk_fintypeproof · cited by 81
Cited by15
Results whose statement or proof uses this declaration.
- Set.encard_singletonproof · cited by 26
- Set.Finite.encard_eq_coe_toFinset_cardproof · cited by 4
- AddCircle.card_torsion_le_of_isSMulRegularproof · cited by 2
- Module.length_finsuppproof · cited by 2
- Set.powersetCard.isPreprimitive_alternatingGroupproof · cited by 2
- IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singletonproof · cited by 1
- SimpleGraph.chromaticNumber_top_eq_enat_cardproof · cited by 0
- Equiv.Perm.isMultiplyPretransitive_of_nontrivialproof · cited by 0
- Matrix.eRank_le_card_widthproof · cited by 0
- SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_enatCardproof · cited by 0
- Convex.helly_theorem_compactproof · cited by 0
- Matrix.eRank_le_card_heightproof · cited by 0