Commit 2023-11-16 06:00 57db954c

View on Github →

chore: remove upstreamed lemmas (#8432)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.length_enum

deleted theorem List.length_enumFrom