Commit 2025-01-10 10:37 a34316ac

View on Github →

chore(Data/Finsupp): split off extensionality from Defs.lean (#19092) These results depend on Submonoid, while nothing else in Finsupp does. So let's move them to their own file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

Modified Mathlib/Data/Finsupp/Defs.lean

deleted theorem Finsupp.addHom_ext'

deleted theorem Finsupp.addHom_ext

deleted theorem Finsupp.add_closure_setOf_eq_single

deleted theorem Finsupp.mulHom_ext'

deleted theorem Finsupp.mulHom_ext

Created Mathlib/Data/Finsupp/Ext.lean

added theorem Finsupp.addHom_ext'

added theorem Finsupp.addHom_ext

added theorem Finsupp.add_closure_setOf_eq_single

added theorem Finsupp.mulHom_ext'

added theorem Finsupp.mulHom_ext