Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-14 15:25 91b099eb

View on Github →

chore(data/equiv/fin): simp definitional lemmas (#5740)

Estimated changes

Modified src/data/equiv/fin.lean

added theorem fin_succ_equiv_succ

added theorem fin_succ_equiv_symm_none

added theorem fin_succ_equiv_symm_some

added theorem fin_succ_equiv_zero