Theorems · Theorem · logic and foundations
Set.ncard_coe_finset
∀ {α : Type u_1} (s : Finset α), (↑s).ncard = s.card- Defined in
- Mathlib.Data.Set.Card
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Finsetstatement and proof · cited by 13,712
- SetLike.coestatement and proof · cited by 8,199
- Finset.cardstatement and proof · cited by 2,327
- Set.ncardstatement · cited by 344
- Set.toFiniteproof · cited by 174
- Set.ncard_eq_toFinset_cardproof · cited by 21
- Finset.finite_toSet_toFinsetproof · cited by 2
Cited by15
Results whose statement or proof uses this declaration.
- Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_memproof · cited by 2
- Set.powersetCard.ncard_eqproof · cited by 2
- Set.exists_subsuperset_card_eqproof · cited by 1
- Equiv.Perm.subgroup_eq_top_of_isPreprimitive_of_isSwap_memproof · cited by 1
- Polynomial.ncard_boxPolyproof · cited by 1
- Set.Infinite.exists_subset_ncard_eqproof · cited by 1
- IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mulproof · cited by 1
- FiniteField.unitsMap_norm_surjectiveproof · cited by 1
- SimpleGraph.odd_ncard_oddComponentsproof · cited by 1
- Set.eq_insert_of_ncard_eq_succproof · cited by 1
- Set.ncard_powerset_ncardproof · cited by 1
- Set.exists_subset_or_subset_of_two_mul_lt_ncardproof · cited by 0