Commit 2026-04-02 14:40 ed4fde18

View on Github →

feat: Bird–Wadler duality theorems (#35713) Forms of these three theorems already exist in mathlib and the Lean standard library, but they are scattered about. Bring them together in one file, deprecating the ad hoc names for the first and second theorems.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.foldl1_eq_foldr1

deleted theorem List.foldl_assoc_comm_cons

deleted theorem List.foldl_eq_foldr'

deleted theorem List.foldl_eq_foldr

deleted theorem List.foldl_eq_of_comm'

deleted theorem List.foldl_eq_of_comm_of_assoc

deleted theorem List.foldl_op_eq_op_foldr_assoc

deleted theorem List.foldr_eq_of_comm'

Created Mathlib/Data/List/Fold.lean

added theorem List.foldl1_eq_foldr1

added theorem List.foldl_cons_eq_apply_foldl

added theorem List.foldl_cons_nil

added theorem List.foldl_eq_foldr

added theorem List.foldl_eq_foldr_of_commute

added theorem List.foldl_flip_eq_foldr

added theorem List.foldr_cons_eq_foldr_apply

added theorem List.foldr_flip_eq_foldl

Modified docs/references.bib