Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-07 15:40 320da57a

View on Github →

chore(data/fintype/basic): add fintype instance for is_empty (#7692)

Estimated changes

Modified src/analysis/mean_inequalities.lean

Modified src/data/fintype/basic.lean

added theorem finset.univ_eq_empty'

added theorem fintype.card_of_is_empty

added theorem fintype.univ_of_is_empty

Modified src/data/fintype/card.lean

Modified test/matrix.lean