Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-09-11 04:48
202f4891
View on Github →
feat(Algebra/BigOperators): product of MulHom over nonempty multisets (
#16602
)
Estimated changes
Modified
Mathlib/Algebra/BigOperators/Group/Multiset.lean
added
theorem
Multiset.prod_hom_ne_zero
added
theorem
Multiset.prod_hom₂_ne_zero
added
theorem
map_multiset_ne_zero_prod