Theorem map_multiset_ne_zero_prod

Modification history

2024-09-11 04:48

Mathlib/Algebra/BigOperators/Group/Multiset.lean

feat(Algebra/BigOperators): product of MulHom over nonempty multisets (#16602)

Added map_multiset_ne_zero_prod View on Github →