Def MonoidHom.fromULiftMultiplicativeIntEquiv

Modification history

2025-12-29 03:44
Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean
chore: remove May 2025 deprecated declarations (#33014) …
Deleted MonoidHom.fromULiftMultiplicativeIntEquivView 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.fromULiftMultiplicativeIntEquivView on Github →