Theorem List.le_prod_nonempty_of_submultiplicative_on_pred

Modification history

2025-11-04 12:44
Mathlib/Algebra/Order/BigOperators/Group/List.lean
feat: add List.le_prod_of_submultiplicative and friends (#31016)
Added List.le_prod_nonempty_of_submultiplicative_on_predView on Github →