Commit 2024-04-23 03:32 cf0d5d44

View on Github →

chore(List): drop primed deprecated lemmas (#12307) Cherry-picked from #9607

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.concat_eq_append'

deleted theorem List.length_concat'

deleted theorem List.subset_append_of_subset_right'

deleted theorem List.take_one_drop_eq_of_lt_length'