Commit 2024-09-30 13:03 d86c1630

View on Github →

feat: add missing List.foldr lemmas (#17222)

Estimated changes

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

modified theorem List.Perm.prod_eq

Modified Mathlib/Data/List/Basic.lean

added theorem List.foldr_assoc

Modified Mathlib/Data/List/Perm.lean

deleted theorem List.Perm.fold_op_eq

added theorem List.Perm.foldl_op_eq

added theorem List.Perm.foldr_eq'

added theorem List.Perm.foldr_op_eq