Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-13 10:17
6d0f7fe0
View on Github →
Feat: Port/data.fin.succ_pred (
#1511
) Port of data.fin.succ_pred to Data.Fin.SuccPred
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/Fin/SuccPred.lean
added
theorem
Fin.pred_apply
added
theorem
Fin.pred_eq
added
theorem
Fin.succ_apply
added
theorem
Fin.succ_eq