Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 11:56 4bcc5325

View on Github →

refactor(control/fold): don't use is_monoid_hom (#13350)

Estimated changes

Modified src/control/fold.lean

modified def monoid.foldl.of_free_monoid

modified def monoid.foldr.of_free_monoid

modified def monoid.mfoldl.of_free_monoid

modified def monoid.mfoldr.of_free_monoid

deleted theorem traversable.fold_foldl

deleted theorem traversable.fold_foldr

deleted theorem traversable.fold_mfoldl

deleted theorem traversable.fold_mfoldr

deleted theorem traversable.free.map.is_monoid_hom

modified def traversable.free.map

modified def traversable.map_fold

deleted theorem traversable.mfoldl.unop_of_free_monoid