Def MonoidHom.precompEquiv

Modification history

2025-01-07 04:59
Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean
chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416) …
Modified MonoidHom.precompEquivView on Github →
2024-12-14 20:37
Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean
feat(Algebra/Category/Grp/ForgetCorepresentable, Algebra/Category/MonCat/ForgetCorepresentable): the forgetful functor on the category of monoids is corepresentable (#19964) …
Modified MonoidHom.precompEquivView on Github →
2024-04-19 14:49
Mathlib/Algebra/Category/GroupCat/ForgetCorepresentable.lean
feat: the forget functor from commutative groups to groups preserves all limits (#11669) …
Added MonoidHom.precompEquivView on Github →