English
Let G and N be groups (with appropriate monoid structures). The map that sends a multiplicative equivalence between G and N to its underlying monoid homomorphism is injective; i.e., two multiplicative equivalences that induce the same monoid homomorphism must be the same.
Русский
Пусть G и N — группы. Отображение, которое сопоставляет мультипликативной эквивалентности между G и N соответствующий ей моноид-гомоморфизм, инъективно; то есть две мультипликативные эквивалентности, порождающие один и тот же гомоморфизм, совпадают.
LaTeX
$$$\forall h_1,h_2\,\big(\operatorname{toMonoidHom}(h_1) = \operatorname{toMonoidHom}(h_2) \Rightarrow h_1 = h_2\big)$$$
Lean4
@[to_additive]
theorem toMonoidHom_injective : Injective (toMonoidHom : M ≃* N → M →* N) :=
Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective
