First isomorphism for rings

Stream: Is there code for X?

[Patrick Massot]

I'm currently writing a new chapter about algebra in #mil and having a section about rings right after a section about groups is pretty painful in how many inconsistencies it reveals. In particular I cannot find

example {R S : Type*} [CommRing R] [CommRing S]  (f : R →+* S) : R ⧸ (RingHom.ker f) ≃+* f.range := sorry

anywhere whereas docs#QuotientGroup.quotientKerEquivRange is easy to find, and there docs#quotientKerEquivOfSurjective. Is the above version really missing?

[Junyan Xu]

docs#RingHom.quotientKerEquivOfSurjective exists but indeed loogle returns no results for RingHom.ker, RingHom.range.

[Kalle Kytölä]

A recent discussion, where I complained (with an oversimplification) about the spelling related to the First isomorphism theorem for (noncommutative) algebras or rings.