Theorem List.eraseIdx_eq_take_drop_succ

Modification history

2024-05-14 03:32
Mathlib/Data/List/Basic.lean
chore: bump dependencies (#12893)
Deleted List.eraseIdx_eq_take_drop_succView on Github →
2024-02-29 18:56
Mathlib/Data/List/Basic.lean
feat: Add norm_iteratedFDeriv_prod_le using Sym (#10022) …
Added List.eraseIdx_eq_take_drop_succView on Github →