Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-24 05:12 56535164

View on Github →

feat(data/fin): some lemmas about casts (#8049) From LTE.

Estimated changes

Modified src/data/fin.lean

added theorem fin.cast_succ_eq_zero_iff

added theorem fin.cast_succ_ne_zero_iff

added theorem fin.cast_succ_pred_eq_pred_cast_succ

added theorem fin.pred_succ_above_pred

added theorem fin.succ_above_eq_zero_iff

added theorem fin.succ_above_ne_zero

added theorem fin.succ_above_ne_zero_zero