Con.ker vs Con.mulKer

Stream: mathlib4

[Eric Wieser]

Which of docs#Con.ker and docs#Con.mulKer should we keep?

[Yury G. Kudryashov]

I would vote for a definition with MulHomClass assumption.

[Kyle Miller]

They seem like they're not comparable. The first is for a MonoidHom (requiring Mul, One, and a proof-carrying monoid homorphism), but the second is for any Mul-preserving function, without any reference to One.

Yury's suggestion of MulHomClass seems good. It would be even better if there were a constructor to easily pass in a function and a proof that it is merely Mul-preserving. (I'm assuming there are applications of Con.mulKer that use plain functions, I didn't check.)

[Eric Wieser]

Right, if we don't keep the Class version, we should weaken the MonoidHom version to MulHom

[Kyle Miller]

(I've somehow never come across MulHom and →ₙ* even though they've been in mathlib for years. That resolves my question "how you you pass in a merely Mul-preserving function to a function that wants a MulHomClass".)

[Eric Wieser]

#23244 merges the two under the ker name using MulHomClass

[Eric Wieser]

I don't know if we really care about the MulHom application, so haven't thought too much about simp-normal forms. The key thing for now is to eliminate the duplicate defs.

[Eric Wieser]

:ping_pong: on #23244

[Yury G. Kudryashov]

Delegated