Commit 2026-10-10 12:26 945c110a

View on Github →

chore: rename Traversable.foldlm/foldrm to foldlM/foldrM (#44641) Renames the monadic folds and their lemmas to the foldlM/foldrM spelling used by core, adding docstrings so their nolints.json entries can go. 🤖 Generated with Claude Code

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean

Modified Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean

Modified Mathlib/Control/Fold.lean

added theorem Traversable.foldlM.ofFreeMonoid_comp_of

added def Traversable.foldlM

added theorem Traversable.foldlM_map

added theorem Traversable.foldlM_toList

deleted theorem Traversable.foldlm.ofFreeMonoid_comp_of

deleted def Traversable.foldlm

deleted theorem Traversable.foldlm_map

deleted theorem Traversable.foldlm_toList

added theorem Traversable.foldrM.ofFreeMonoid_comp_of

added def Traversable.foldrM

added theorem Traversable.foldrM_map

added theorem Traversable.foldrM_toList

deleted theorem Traversable.foldrm.ofFreeMonoid_comp_of

deleted def Traversable.foldrm

deleted theorem Traversable.foldrm_map

deleted theorem Traversable.foldrm_toList

Modified scripts/nolints.json