Def CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers

Modification history

2023-07-12 03:49

Mathlib/CategoryTheory/Monad/Monadicity.lean

feat: port CategoryTheory.Monad.Monadicity (#5088)

Added CategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers View on Github →