ZMod.lift for ring homs

Stream: Is there code for X?

[Adam Topaz]

Do we have an analogue of docs#ZMod.lift that gives the universal property with respect to morphisms of rings?

[Adam Topaz]

We have docs#Int.quotientSpanNatEquivZMod but it seems that there is no associated ZMod.liftRingHom

[Michael Stoll]

docs#ZMod.castHom should do it.

[Adam Topaz]

Great!

[Adam Topaz]

Thanks!

[Michael Stoll]

That's how I found it:
@loogle ZMod, Dvd.dvd, "hom"

[loogle]

:search: ZMod.castHom, ZMod.castHom_comp, and 2 more

[Adam Topaz]

Huh, I tried loogle as well, but it came up short.