Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-11 08:22 840a0425

View on Github →

feat(data/list/basic): Miscellaneous fold lemmas (#12579)

Estimated changes

Modified src/data/list/basic.lean

added theorem list.foldl_combinator_K

added theorem list.foldl_fixed

added theorem list.foldr_fixed

Modified src/logic/function/iterate.lean

added theorem list.foldl_const

added theorem list.foldr_const