Mathlib v3 is deprecated. Go to Mathlib v4

Def fin_one_equiv

Modification history

2021-05-18 04:50

src/data/equiv/fin.lean

feat(logic/is_empty): Add is_empty typeclass (#7606) …

Modified fin_one_equiv View on Github →

2018-10-17 13:50

data/equiv/fin.lean

chore(data/fin): use uniform names; restructure

Added fin_one_equiv View on Github →