Commit 2024-12-20 05:03 024a16f8

View on Github →

chore(Data/List/AList): Rename insert_of_neg and similar to insert_of_not_mem (#19960) completes a todo, also mentioned in #7987 also deprecates the old things

Estimated changes

Modified Mathlib/Data/Finmap.lean

added theorem Finmap.entries_insert_of_not_mem

deleted theorem Finmap.insert_entries_of_neg

Modified Mathlib/Data/List/AList.lean

added theorem AList.entries_insert

added theorem AList.entries_insert_of_not_mem

deleted theorem AList.insert_entries

deleted theorem AList.insert_entries_of_neg

deleted theorem AList.insert_of_neg

added theorem AList.insert_of_not_mem