Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-26 16:48 5afdaea4

View on Github →

feat(data/fin): reverse_induction (#8845)

Estimated changes

Modified src/data/fin.lean

added def fin.last_cases

added theorem fin.last_cases_cast_succ

added theorem fin.last_cases_last

added def fin.reverse_induction

added theorem fin.reverse_induction_cast_succ

added theorem fin.reverse_induction_last