Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-22 22:06 c4132e9a

View on Github →

chore(logic/unique): add fin.inhabited (#5077)

Estimated changes

Modified src/data/fin.lean

deleted theorem fin.default_fin_one

Modified src/logic/unique.lean

added theorem fin.default_eq_zero

added theorem fin.eq_zero

added def pi.unique_of_empty