Image of a monoid hom is a monoid

Stream: Is there code for X?

[Philipp Weisang]

I found such a result for additive monoids but I need it for mulitplicative monoids.

[Floris van Doorn]

docs#Function.Surjective.monoid ?

[Floris van Doorn]

or perhaps you mean docs#MonoidHom.mrange ?
Hint: try to state what you want in Lean. That is a good exercise, and clarifies what you want exactly (and sometimes by exact? will even find it)

[Floris van Doorn]

(there is also docs#Submonoid.map )

[Philipp Weisang]

Thanks for the response.
I see how both of these can be used for what i need but it seems to me there should simply be a proof of something like

variable {M N : Type*} [Monoid M] [Monoid N]
variable (L : Set M) (ϕ : M →* N)
instance im_is_mon :
     Monoid (ϕ.mrange) :=

[Junyan Xu]

inferInstance should already work? (because of SubmonoidClass.toMonoid)

[Philipp Weisang]

Pretty much. This worked for me:

instance im_is_mon :
     Monoid (MonoidHom.mrange ϕ) := by infer_instance

Thank you.