Commit 2024-07-20 03:37 8f84584e

View on Github →

chore(CategoryTheory/Monad): rename η' to η (#14886) There are no differences between η' and η (unit for the monad T) anymore as we have a syntactic tautology T.toFunctor = T in Lean 4.

Estimated changes

Modified Mathlib/CategoryTheory/Monad/Adjunction.lean

Modified Mathlib/CategoryTheory/Monad/Basic.lean

deleted def CategoryTheory.Comonad.Simps.coe

deleted def CategoryTheory.Comonad.Simps.δ

deleted def CategoryTheory.Comonad.Simps.ε

deleted theorem CategoryTheory.Comonad.coassoc

deleted theorem CategoryTheory.Comonad.left_counit

deleted theorem CategoryTheory.Comonad.right_counit

deleted def CategoryTheory.Comonad.δ

deleted def CategoryTheory.Comonad.ε

deleted def CategoryTheory.Monad.Simps.coe

deleted def CategoryTheory.Monad.Simps.η

deleted def CategoryTheory.Monad.Simps.μ

deleted theorem CategoryTheory.Monad.assoc

deleted theorem CategoryTheory.Monad.left_unit

deleted theorem CategoryTheory.Monad.right_unit

deleted def CategoryTheory.Monad.η

deleted def CategoryTheory.Monad.μ

Modified Mathlib/CategoryTheory/Monad/EquivMon.lean

Modified Mathlib/CategoryTheory/Monad/Products.lean

Modified Mathlib/CategoryTheory/Monad/Types.lean

Modified Mathlib/MeasureTheory/Category/MeasCat.lean