Commit 2024-10-14 08:17 5ab87a97

View on Github →

chore: use foldr in List.prod (#17223) Makes List.prod_cons a rfl lemma, without any axioms. Closes https://github.com/leanprover-community/mathlib3/issues/161 Simplifies some hypotheses, and makes this compatible with Nat.sum in core (which I will subsequently remove).

Estimated changes

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

modified theorem List.Perm.prod_eq

modified theorem List.prod_cons

added theorem List.prod_eq_foldl

modified theorem List.prod_eq_foldr

modified theorem Nat.sum_eq_listSum

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

modified theorem Multiset.prod_coe

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

Modified Mathlib/Data/Finsupp/BigOperators.lean

Modified Mathlib/Data/PNat/Factors.lean