Monoid hom from Nat given by AddMonoid element

Stream: Is there code for X?

[Scott Carnahan]

I couldn't find the following:

import Mathlib.Algebra.Group.Nat

def nsmul.MonoidHom {Γ : Type*} [AddMonoid Γ] (g : Γ) : ℕ →+ Γ where
  toFun n := n • g
  map_zero' := zero_nsmul g
  map_add' := add_nsmul g

Does this have a place in mathlib, or should I use something like an anonymous constructor?

[Yury G. Kudryashov]

See docs#multiplesHom

[Yury G. Kudryashov]

Found by @loogle Nat →+ _

[loogle]

:search: multiplesHom, Nat.castAddMonoidHom, and 15 more

[Yury G. Kudryashov]

It's an Equiv, not a constructor, so it doesn't appear in @loogle |- Nat →+ _

[loogle]

:search: Nat.castAddMonoidHom, Multiset.replicateAddMonoidHom

[Scott Carnahan]

Thank you!