Card

📁 Source: Mathlib/Data/Sym/Card.lean

Statistics

Metric	Count
Definitions e1, e2	2
Theorems card_sym_eq_choose, card_sym_eq_multichoose, card_sym_fin_eq_multichoose, card, card_diagSet_compl, card_image_diag, card_image_offDiag, card_subtype_diag, card_subtype_not_diag, two_mul_card_image_offDiag	10
Total	12

Sym

Definitions

Name	Category	Theorems
e1 📖	CompOp	—
e2 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_sym_eq_choose 📖	mathematical	—	Fintype.card Sym Nat.choose	—	card_sym_eq_multichoose Nat.multichoose_eq
card_sym_eq_multichoose 📖	mathematical	—	Fintype.card Sym Nat.multichoose	—	card_sym_fin_eq_multichoose Fintype.card_congr
card_sym_fin_eq_multichoose 📖	mathematical	—	Fintype.card Sym instFintypeSymOfDecidableEq Fin.fintype Nat.multichoose	—	—

Sym2

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Fintype.card Sym2 instFintype Nat.choose	—	Finset.card_sym2
card_diagSet_compl 📖	mathematical	—	Fintype.card Set.Elem Sym2 Compl.compl Set Set.instCompl diagSet Subtype.fintype Set.instMembership Set.decidableCompl decidablePred_mem_diagSet instFintype Nat.choose	—	card_subtype_not_diag
card_image_diag 📖	mathematical	—	Finset.card Sym2 Finset.image instDecidableEq Finset.diag	—	Finset.image_diag Finset.card_image_of_injOn
card_image_offDiag 📖	mathematical	—	Finset.card Sym2 Finset.image instDecidableEq Finset.offDiag Nat.choose	—	Nat.choose_two_right mul_one Finset.offDiag_card two_mul_card_image_offDiag
card_subtype_diag 📖	mathematical	—	Fintype.card Sym2 IsDiag Subtype.fintype IsDiag.decidablePred instFintype	—	filter_image_mk_isDiag Fintype.card_of_subtype Finset.mem_filter Finset.univ_product_univ Finset.mem_image Finset.mem_univ card_image_diag
card_subtype_not_diag 📖	mathematical	—	Fintype.card Sym2 IsDiag Subtype.fintype IsDiag.decidablePred instFintype Nat.choose	—	filter_image_mk_not_isDiag Fintype.card_of_subtype Finset.mem_filter Finset.univ_product_univ Finset.mem_image Finset.mem_univ card_image_offDiag
two_mul_card_image_offDiag 📖	mathematical	—	Finset.card Sym2 Finset.image instDecidableEq Finset.offDiag	—	Finset.card_eq_sum_card_image Finset.sum_const_nat ind Finset.cons_eq_insert Finset.ext Finset.card_insert_of_notMem Finset.card_singleton mul_comm

---

← Back to Index