English
Let e: α ≃ β. If β has a Monoid structure, α can be endowed with a transported Monoid structure using the transported multiplication and identity.
Русский
Пусть e: α ≃ β. Если β имеет структуру моноида, то α может получить перенесённую структуру моноида с использованием перенесённого умножения и единицы.
LaTeX
$$$\text{Monoid}_\alpha \text{ with } a \star b := e^{-1}(e(a)\cdot e(b)), \ 1_\alpha := e^{-1}(1_β)$$$
Lean4
/-- Transfer `Monoid` across an `Equiv` -/
@[to_additive /-- Transfer `AddMonoid` across an `Equiv` -/
]
protected abbrev monoid [Monoid β] : Monoid α := by
let one := e.one
let mul := e.mul
let pow := e.pow ℕ
apply e.injective.monoid _ <;> intros <;> exact e.apply_symm_apply _
