Commit 2024-01-01 22:36 2a17457d

View on Github →

feat: missing lemmas about Finsupp.update (#9316)

Estimated changes

Modified Mathlib/Data/Finsupp/Defs.lean

added theorem Finsupp.erase_eq_update_zero

added theorem Finsupp.erase_idem

added theorem Finsupp.erase_update_eq_erase

added theorem Finsupp.erase_update_of_ne

added theorem Finsupp.support_update_subset

added theorem Finsupp.update_comm

added theorem Finsupp.update_erase_eq_update

added theorem Finsupp.update_idem