Def CategoryTheory.Monad.Algebra.algebraFunctorOfMonadHomEq

Modification history

2026-10-17 22:47

Mathlib/CategoryTheory/Monad/Algebra.lean

chore(CategoryTheory/Monad): use `to_dual` (#44628) …

Added CategoryTheory.Monad.Algebra.algebraFunctorOfMonadHomEq View on Github →