Mathlib Map

Theorems · Theorem · logic and foundations

Nat.card_coe_set_eq

∀ {α : Type u_1} (s : Set α), Nat.card ↑s = s.ncard
Defined in
Mathlib.Data.Set.Card
Cited by
19 results in Mathlib
Foundations
Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.ncard_eq_toFinset_card · cited by 21Set.ncard_eq_toFinset_cardSet.Infinite.ncard · cited by 12Infinite.ncardMulAction.index_stabilizer · cited by 4MulAction.index_stabilizerAddAction.index_stabilizer · cited by 3AddAction.index_stabilizerMonoidHom.surjective_of_card_ker_le_div · cited by 2MonoidHom.surjective_of_c…Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card · cited by 2Embedding.exists_embeddin…Set.powersetCard.nontrivial · cited by 2powersetCard.nontrivialPi.dim_spanSubset · cited by 2Pi.dim_spanSubsetSubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter · cited by 1IsPreprimitive.isPreprimi…Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial · cited by 1IsStandardSmoothOfRelativ…FiniteField.unitsMap_norm_surjective · cited by 1FiniteField.unitsMap_norm…AddSubgroup.IsComplement.ncard_left · cited by 1IsComplement.ncard_leftAddSubgroup.IsComplement.ncard_right · cited by 1IsComplement.ncard_rightEquiv.Perm.has_swap_mem_of_lt_stabilizer · cited by 1Perm.has_swap_mem_of_lt_s…Subgroup.IsComplement.ncard_left · cited by 1IsComplement.ncard_leftSet · cited by 53352SetSet.Elem · cited by 7166Set.ElemNat.card · cited by 844Nat.cardSet.ncard · cited by 344Set.ncardNat.card_coe_set_eqCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Set.Elemstatement · cited by 7,166
  • Nat.cardstatement · cited by 844
  • Set.ncardstatement · cited by 344

Cited by19

Results whose statement or proof uses this declaration.