Surjectivity of (ZMod m)ˣ →* (ZMod n)ˣ

Stream: Is there code for X?

[Michael Stoll]

Do we have a statement equivalent to

lemma ZMod.unitsMap_surjective {n m : ℕ} (h : n ∣ m) (hm : m ≠ 0) : Function.Surjective (ZMod.unitsMap h)

(where

def ZMod.unitsMap {n m : ℕ} (hm : n ∣ m) : (ZMod m)ˣ →* (ZMod n)ˣ :=
  Units.map (ZMod.castHom hm (ZMod n))

-- this was added recently)?

I.e. the canonical homomorphism from $\mathbb Z/m \mathbb Z$ to $\mathbb Z/n \mathbb Z$ is surjective on units (when $n$ divides $m$ and $m \neq 0$).

[Alex J. Best]

I have a feeling this was discussed a long time ago but I can't find the thread unfortunately :confused:.
At the time I thought formalizing the notion of a semilocal ring (and some of the material in https://mathoverflow.net/questions/31495/when-does-a-ring-surjection-imply-a-surjection-of-the-group-of-units) would be a nice way to get this, but its a bit overkill of course.

[Michael Stoll]

Maybe this could be a nice project for somebody... (I don't have time right now).