English
Postcomposition with an equivalence e : α ≃* β yields an equivalence between γ →* α and γ →* β.
Русский
Посткомпозиция с эквивалентностью e : α ≃* β даёт эквивалентность между γ →* α и γ →* β.
LaTeX
$$$ (\gamma \to^* \alpha) \simeq (\gamma \to^* \beta) \quad\text{via } f \mapsto e \circ f, \; g \mapsto e^{-1} \circ g. $$$
Lean4
/-- The equivalence `(β →* γ) ≃ (α →* γ)` obtained by precomposition with
a multiplicative equivalence `e : α ≃* β`. -/
@[to_additive (attr := simps -isSimp, deprecated MulEquiv.monoidHomCongrLeftEquiv (since := "2025-08-12")) /--
The equivalence `(β →+ γ) ≃ (α →+ γ)` obtained by precomposition with
an additive equivalence `e : α ≃+ β`. -/
]
def precompEquiv {α β : Type*} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type*) [Monoid γ] : (β →* γ) ≃ (α →* γ)
where
toFun f := f.comp e
invFun g := g.comp e.symm
left_inv _ := by ext; simp
right_inv _ := by ext; simp
