Theorem Multiset.prod_hom₂_ne_zero

Modification history

2024-09-11 04:48
Mathlib/Algebra/BigOperators/Group/Multiset.lean
feat(Algebra/BigOperators): product of MulHom over nonempty multisets (#16602)
Added Multiset.prod_hom₂_ne_zeroView on Github →