Commit 2024-09-09 01:17 5f1b34c8

View on Github →

feat(Algebra/Order/BigOperators): prove lemmas for List.prod and Multiset.prod on CommMonoidWithZero (#16573) Also relax typeclass assumptions on prod_nonneg.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/BigOperators/GroupWithZero/List.lean

added theorem List.one_le_prod

added theorem List.prod_map_le_prod_map₀

added theorem List.prod_map_lt_prod_map

added theorem List.prod_nonneg

added theorem List.prod_pos

Created Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean

added theorem Multiset.one_le_prod

added theorem Multiset.prod_map_le_prod_map₀

added theorem Multiset.prod_map_lt_prod_map

added theorem Multiset.prod_nonneg

added theorem Multiset.prod_pos

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

modified theorem CanonicallyOrderedCommSemiring.list_prod_pos

deleted theorem List.prod_pos

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

modified theorem CanonicallyOrderedCommSemiring.multiset_prod_pos

deleted theorem Multiset.prod_nonneg