Commit 2026-06-09 17:40 94501fd4

View on Github →

chore: remove duplicate of List.take_one_drop_eq_of_lt_length (#40422) Leave the other copy in Mathlib.Data.List.TakeDrop. Follow-up to #21232. Deletions:

  • List.take_one_drop_eq_of_lt_length

Estimated changes