Commit 2023-06-24 17:10 177ae4e9

View on Github →

feat: relate List.mapAccumr to List.foldr (#5390) Add lemmas that rewrite an application of List.mapAccumr or List.mapAccumr_2 into an application of List.foldr

Estimated changes

Modified Mathlib/Data/List/Lemmas.lean

added theorem List.mapAccumr_eq_foldr

added theorem List.mapAccumr₂_eq_foldr