Theorem Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg

Modification history

2025-04-30 16:43
Mathlib/Algebra/Order/BigOperators/Ring/Multiset.lean
feat(Algebra/Order/BigOperator): add lemmas (#23266)
Added Multiset.le_prod_of_submultiplicative_on_pred_of_nonnegView on Github →