Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-16 16:19 a55084f5

View on Github →

feat(data/fintype/basic): card_sum, card_subtype_or (#8490)

Estimated changes

Modified src/data/fintype/basic.lean

added theorem fintype.card_subtype

added theorem fintype.card_subtype_or

added theorem fintype.card_subtype_or_disjoint

added theorem fintype.card_sum

Modified src/data/fintype/card.lean

deleted theorem fintype.card_sum