Commit 2023-05-08 03:29 b429db2e

View on Github →

feat: port Data.Sym.Card (#3109)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Sym/Card.lean

added theorem Finset.card_sym2

added theorem Sym.card_sym_eq_choose

added theorem Sym.card_sym_eq_multichoose

added theorem Sym.card_sym_fin_eq_multichoose

added theorem Sym2.card_image_diag

added theorem Sym2.card_image_offDiag

added theorem Sym2.card_subtype_diag

added theorem Sym2.card_subtype_not_diag

added theorem Sym2.two_mul_card_image_offDiag