mathlib

7ee41aab - feat(data/finsupp/basic): lemmas about map domain with only inj_on hypotheses (#11484)

feat(data/finsupp/basic): lemmas about map domain with only inj_on hypotheses (#11484) Also a lemma `sum_update_add` expressing the sum of an update in a monoid in terms of the original sum and the value of the update. And golf `map_domain_smul`. From flt-regular.