Commit 2024-04-17 12:17 1342b9e1

View on Github →

feat(Function/Support): support of update (#11736) Generalize 4 lemmas from Finsupp to Function.

Estimated changes

Modified Mathlib/Algebra/Function/Support.lean

added theorem Function.ext_iff_mulSupport

added theorem Function.mulSupport_update_eq_ite

added theorem Function.mulSupport_update_of_ne_one

added theorem Function.mulSupport_update_one