English
The left-congruence equivalence e ↦ monoidHomCongrLeftEquiv e is an isomorphism between the relevant Hom-sets.
Русский
Левая конгруэнтная эквивалентность e ↦ monoidHomCongrLeftEquiv e образует изоморфизм между соответствующими множествами гомоморфизмов.
LaTeX
$$$\text{Isomorphism: } e \mapsto e.monoidHomCongrLeftEquiv$$$
Lean4
/-- The isomorphism `(M₁ →* N) ≃* (M₂ →* N)` obtained by postcomposition with
a multiplicative equivalence `e : M₁ ≃* M₂`. -/
@[to_additive (attr := simps! apply) /-- The isomorphism `(M₁ →+ N) ≃+ (M₂ →+ N)` obtained by postcomposition with
an additive equivalence `e : M₁ ≃+ M₂`. -/
]
def monoidHomCongrLeft (e : M₁ ≃* M₂) : (M₁ →* N) ≃* (M₂ →* N)
where
__ := e.monoidHomCongrLeftEquiv
map_mul' f g := by ext; simp
