Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-12 08:32 1b96e977

View on Github →

feat(data/sym2): card of sym2 α (#8426) Case n = 2 of stars and bars

Estimated changes

Created src/data/sym/card.lean

added theorem sym2.card_image_diag

added theorem sym2.card_image_off_diag

added theorem sym2.card_subtype_diag

added theorem sym2.card_subtype_not_diag

added theorem sym2.two_mul_card_image_off_diag

Modified src/data/sym/sym2.lean

added theorem sym2.diag_injective

added theorem sym2.filter_image_quotient_mk_is_diag

added theorem sym2.filter_image_quotient_mk_not_is_diag