English
The composition of two unit maps corresponds to the transitive reduction of divisors: unitsMap hm composed with unitsMap hd equals unitsMap (dvd_trans hm hd).
Русский
Составление двух отображений единиц соответствует тривиальной редукции делителей: unitsMap hm ∘ unitsMap hd = unitsMap (dvd_trans hm hd).
LaTeX
$$$$ (unitsMap hm).comp (unitsMap hd) = unitsMap (dvd\\_trans hm hd). $$$$
Lean4
theorem unitsMap_comp {d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
(unitsMap hm).comp (unitsMap hd) = unitsMap (dvd_trans hm hd) :=
by
simp only [unitsMap_def]
rw [← Units.map_comp]
exact congr_arg Units.map <| congr_arg RingHom.toMonoidHom <| castHom_comp hm hd
