English
Equality compatibility of postcompEquiv with the structure of MonoidHom.
Русский
Совместимость посткомпозиции с структурой MonoidHom в равенствах.
LaTeX
$$$ MonoidHom.postcompEquiv e γ \; {\; toFun := \dots, invFun := \dots } $$$
Lean4
/-- The equivalence `(γ →* α) ≃ (γ →* β)` obtained by postcomposition with
a multiplicative equivalence `e : α ≃* β`. -/
@[to_additive (attr := simps -isSimp, deprecated MulEquiv.monoidHomCongrRightEquiv (since := "2025-08-12")) /--
The equivalence `(γ →+ α) ≃ (γ →+ β)` obtained by postcomposition with
an additive equivalence `e : α ≃+ β`. -/
]
def postcompEquiv {α β : Type*} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type*) [Monoid γ] : (γ →* α) ≃ (γ →* β)
where
toFun f := e.toMonoidHom.comp f
invFun g := e.symm.toMonoidHom.comp g
left_inv _ := by ext; simp
right_inv _ := by ext; simp
