Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-05 01:27 530e7e32

View on Github →

chore(data/quot): rename nonempty_of_trunc to enable dot notation (#7034)

Estimated changes

Modified src/data/fintype/basic.lean

Modified src/data/quot.lean

deleted theorem nonempty_of_trunc

Modified src/data/set/countable.lean