Commit 2024-04-23 03:32 65e0bd6f

View on Github →

chore(List): drop some deprecated lemmas (#12306) Cherry-picked from #9607

Estimated changes

Modified Mathlib/Data/List/Enum.lean

deleted theorem List.nthLe_enum

deleted theorem List.nthLe_enumFrom

Modified Mathlib/Data/List/GetD.lean

deleted theorem List.getD_eq_nthLe

deleted theorem List.getI_eq_nthLe