Theorem Fin.castLE_castSucc

Modification history

2025-09-04 06:44

Mathlib/Data/Fin/Basic.lean

chore(Data/Fin/Basic): Split lemmas on `succ` and `pred`. (#29199) …

Modified Fin.castLE_castSucc View on Github →

2023-11-11 11:20

Mathlib/Data/Fin/Basic.lean

feat: Add to `List.finRange` and `Fin.castLE` APIs (#8306) …

Added Fin.castLE_castSucc View on Github →