Commit 2025-11-04 12:44 ae1cfd83

View on Github →

feat: add List.le_prod_of_submultiplicative and friends (#31016)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/List/Defs.lean

added theorem List.prod_induction_nonempty

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

modified theorem Finset.le_prod_of_submultiplicative

Modified Mathlib/Algebra/Order/BigOperators/Group/List.lean

added theorem List.le_prod_nonempty_of_submultiplicative

added theorem List.le_prod_nonempty_of_submultiplicative_on_pred

added theorem List.le_prod_of_submultiplicative

added theorem List.le_prod_of_submultiplicative_on_pred

Modified Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

modified theorem Multiset.le_prod_of_submultiplicative

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

Modified Mathlib/Algebra/Order/Interval/Basic.lean

Modified Mathlib/Analysis/Convex/Gauge.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean