Theorem Finsupp.addCommute_of_disjoint

Modification history

2025-09-06 21:16
Mathlib/Algebra/Group/Finsupp.lean
feat: finsupps with disjoint support commute (#28761) …
Added Finsupp.addCommute_of_disjointView on Github →