monoid_hom from mul_hom?

Stream: Is there code for X?

[Scott Morrison]

Do we have the constructor that promotes a mul_hom to a monoid_hom when the source and target are groups?

[Scott Morrison]

(I guess the source only needs to be a monoid?)

[Yaël Dillies]

I would expect it to be called mul_hom.to_monoid_hom, so it seems like we don't. However, we do have docs#is_mul_hom.to_is_monoid_hom

[Scott Morrison]

In the olden days we had is_mul_hom.to_is_monoid_hom for this.

[Eric Wieser]

docs#monoid_hom.mk'?

[Eric Rodriguez]

Can fun_likedo this automatically, BTW?

[Yaël Dillies]

Not until Lean 4, because typeclass loop.

[Eric Wieser]

Not quite a single argument, but monoid_hom.mk' f f.map_mul probably works.

[Eric Wieser]

I'm not convinced we want this to happen automatically anyway

[Yaël Dillies]

I believe we should change monoid_hom.mk' to use mul_hom

[Yaël Dillies]

We do, Eric, we do.

[Yaël Dillies]

Typically, for stuff like branch#GroupWithZero_equiv_Group

[Eric Wieser]

Does whether it's "automatic" or explicit really make much difference there?

[Yaël Dillies]

Eh, I guess not

[Eric Wieser]

Automatic is best for things that are unambiguous, unsurprising, and frequent