Def MonoidHom.fromMultiplicativeNatEquiv

Modification history

2025-05-12 07:47

Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean

chore: deduplicate equivalence `M ≃ (ℕ →+ M)` for `M` an additive monoid (#24783) …

Modified MonoidHom.fromMultiplicativeNatEquiv View on Github →

2024-12-14 20:37

Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean

feat(Algebra/Category/Grp/ForgetCorepresentable, Algebra/Category/MonCat/ForgetCorepresentable): the forgetful functor on the category of monoids is corepresentable (#19964) …

Added MonoidHom.fromMultiplicativeNatEquiv View on Github →