Def AddMonoidHom.fromNatEquiv

Modification history

2025-12-29 03:44
Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean
chore: remove May 2025 deprecated declarations (#33014) …
Deleted AddMonoidHom.fromNatEquivView on Github →
2025-05-12 07:47
Mathlib/Algebra/Category/MonCat/ForgetCorepresentable.lean
chore: deduplicate equivalence `M ≃ (ℕ →+ M)` for `M` an additive monoid (#24783) …
Modified AddMonoidHom.fromNatEquivView 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 AddMonoidHom.fromNatEquivView on Github →