Theorem List.le_prod_of_submultiplicative

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_of_submultiplicative View on Github →