Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-29 13:28 0858157a

View on Github →

refactor(category_theory/category): reorder arguments of End.has_mul (#1128)

Reorder arguments of End.has_mul and Aut.has_mul, adjust category/fold
clean up proofs in category.fold

Estimated changes

Modified src/category/fold.lean

added def monoid.foldl.get

modified def monoid.foldl.mk

modified def monoid.foldl

modified def monoid.foldr.get

modified def monoid.foldr.mk

modified def monoid.foldr

added def monoid.mfoldl.get

modified def monoid.mfoldl.mk

modified def monoid.mfoldl

modified def monoid.mfoldr.get

modified def monoid.mfoldr.mk

added theorem traversable.foldl.unop_of_free_monoid

deleted theorem traversable.foldr.unop_of_free_monoid

added theorem traversable.mfoldl.unop_of_free_monoid

deleted theorem traversable.mfoldr.unop_of_free_monoid

Modified src/category_theory/category.lean

modified theorem category_theory.End.mul_def

Modified src/category_theory/isomorphism.lean

Modified src/data/opposite.lean

added theorem opposite.op_inj_iff

added theorem opposite.unop_inj_iff