Commit 2023-11-11 11:20 d8a661e5

View on Github →

feat: Add to List.finRange and Fin.castLE APIs (#8306) Add a lemma that unfolds finRange n.succ in terms of List.concat, and add a few simp-lemmas for Fin.castLE

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.castLE_castSucc

added theorem Fin.castLE_comp_castSucc

added theorem Fin.castLE_rfl

Modified Mathlib/Data/List/FinRange.lean

added theorem List.finRange_succ