Commit 2024-04-24 08:44 72b62afe

View on Github →

chore(Data/List/Basic): remove some long-deprecated unused lemmas (#12367)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.nthLe_attach

Modified Mathlib/Data/List/Nodup.lean

deleted theorem List.nthLe_eq_of_ne_imp_not_nodup

Modified Mathlib/Data/List/Perm.lean

deleted theorem List.Perm.erasep