zmod.cast_hom

Stream: maths

[Johan Commelin]

Currently zmod.cast_hom is a ring hom from zmod n to rings R with characteristic n. I'm generalising that to rings with characteristic m where m \| n.
But arguable, there should also be a group hom version of cast. How should it be set up? Which should it take as arguments an element whose order divides n?

[Kevin Buzzard]

I don't know the lingo, but would computer scientists still call that a cast?

[Johan Commelin]

Maybe not...

[Johan Commelin]

#2900