Commit 2025-01-13 13:56 71b88c46

chore(Data/Finsupp): split off material on single, update, erase (#19087) To clean up Mathlib.Algebra.MonoidAlgebra.Defs I would like to move material on single from Mathlib.Data.Finsupp.Basic into a smaller file. Although the specific lemmas could go into Mathlib.Data.Finsupp.Defs, that file is already rather big, so instead let's split off a file that sits in between Defs and Basic.