Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin.last_cases_cast_succ

Modification history

2021-08-26 16:48
src/data/fin.lean
feat(data/fin): reverse_induction (#8845)
Added fin.last_cases_cast_succView on Github →