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