English
The isomorphism between MonoidHom M →* N1 and MonoidHom M →* N2 is given by postcomposition with e : N1 ≃* N2.
Русский
Изоморфизм между MonoidHom M →* N1 и MonoidHom M →* N2 задаётся посткомпозицией с e : N1 ≃* N2.
LaTeX
$$$ (M \to^* N_1) \cong^* (M \to^* N_2) \quad\text{via } f \mapsto e \circ f, \; g \mapsto e^{-1} \circ g. $$$
Lean4
/-- The isomorphism `(M →* N₁) ≃* (M →* N₂)` obtained by postcomposition with
a multiplicative equivalence `e : N₁ ≃* N₂`. -/
@[to_additive (attr := simps! apply) /-- The isomorphism `(M →+ N₁) ≃+ (M →+ N₂)` obtained by postcomposition with
an additive equivalence `e : N₁ ≃+ N₂`. -/
]
def monoidHomCongrRight (e : N₁ ≃* N₂) : (M →* N₁) ≃* (M →* N₂)
where
__ := e.monoidHomCongrRightEquiv
map_mul' f g := by ext; simp
