English
Two multiplicative isomorphisms are equal if they agree on every element of the domain.
Русский
Две мультипликативные эквиваленты равны, если они совпадают на каждом элементе области определения.
LaTeX
$$$$\\forall x,\, f x = g x \\Rightarrow f = g.$$$$
Lean4
/-- A multiplicative analogue of `Equiv.arrowCongr`,
for multiplicative maps from a monoid to a commutative monoid.
-/
@[to_additive (attr := deprecated MulEquiv.monoidHomCongrLeft (since := "2025-08-12")) /--
An additive analogue of `Equiv.arrowCongr`,
for additive maps from an additive monoid to a commutative additive monoid. -/
]
def monoidHomCongr {M N P Q} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) :
(M →* P) ≃* (N →* Q) :=
f.monoidHomCongrLeft.trans g.monoidHomCongrRight
