AlgHom kernel

Stream: mathlib4

[Artie Khovanov]

In a few places in the library (eg Mathlib.RingTheory.FinitePresentation), there is extensive use of RingHom.ker f.toRingHom, where f is an AlgHom. However, RingHom.ker takes a RingHomClass, so the .toRingHom is redundant.
Am I OK to refactor it out, or is this usage somehow secretly load-bearing?

[Eric Wieser]

This is the thing I was describing in the other thread; arguably it was a design error to define RingHom.ker to take RingHomClass

[Artie Khovanov]

OK I won't touch it unless I have to