Theorem CategoryTheory.Monad.isSplitMono_iff_isIso_unit

Modification history

2024-10-27 10:17
Mathlib/CategoryTheory/Monad/Basic.lean
feat(CategoryTheory/Monoidal): Day's reflection theorem (#15894)
Added CategoryTheory.Monad.isSplitMono_iff_isIso_unitView on Github →