Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-06 05:50 4192612b

View on Github →

chore(data/fintype/basic): add card_unique and a warning note to card_of_subsingleton (#7008)

Estimated changes

added theorem fintype.card_unique