Theorems · Theorem · logic and foundations
ENat.card_eq_coe_natCard
∀ (α : Type u_4) [Finite α], ENat.card α = ↑(Nat.card α)
- Defined in
- Mathlib.SetTheory.Cardinal.NatCard
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Finite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENatstatement · cited by 4,985
- Finitestatement and proof · cited by 3,029
- Nat.cardstatement · cited by 844
- ENat.cardstatement · cited by 89
- symmproof · cited by 48
- Nat.cast_cardproof · cited by 3
- Cardinal.natCast_eq_toENatproof · cited by 2
Cited by12
Results whose statement or proof uses this declaration.
- Fin.Embedding.restrictSurjective_of_add_le_natCardproof · cited by 3
- Set.powersetCard.fixedPoints_ne_univ_of_faithfulSMulproof · cited by 3
- Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_cardproof · cited by 2
- Set.powersetCard.nontrivialproof · cited by 2
- Set.powersetCard.nontrivial'proof · cited by 1
- Equiv.Perm.has_swap_mem_of_lt_stabilizerproof · cited by 1
- ENNReal.toReal_enatCardproof · cited by 1
- List.Nodup.length_le_enatCardproof · cited by 1
- SimpleGraph.vertexCoverNum_lt_cardproof · cited by 0
- ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomialproof · cited by 0
- SimpleGraph.IsBipartite.four_mul_encard_edgeSet_leproof · cited by 0
- Fin.Embedding.exists_embedding_disjoint_range_of_add_le_Nat_cardproof · cited by 0