Theorem Finsupp.support_update_subset

Modification history

2024-08-01 01:16
Mathlib/Data/Finsupp/Defs.lean
chore(Data/Finsupp/Defs): remove superfluous DecidableEq (#15301) …
Modified Finsupp.support_update_subsetView on Github →
2024-01-01 22:36
Mathlib/Data/Finsupp/Defs.lean
feat: missing lemmas about `Finsupp.update` (#9316)
Added Finsupp.support_update_subsetView on Github →