English
Let e: α ≃ β. If β is a CommGroup, α inherits a transported CommGroup structure via the transported operations.
Русский
Пусть e: α ≃ β. Если β является коммогруппой, α получает перенесённую коммогруппу через перенесённые операции.
LaTeX
$$$\text{CommGroup}_\alpha \text{ with } a \star b := e^{-1}(e(a)\cdot e(b)), \ inv_\alpha(a) := e^{-1}(e(a)^{-1})$$$
Lean4
/-- Transfer `CommGroup` across an `Equiv` -/
@[to_additive /-- Transfer `AddCommGroup` across an `Equiv` -/
]
protected abbrev commGroup [CommGroup β] : CommGroup α :=
by
let one := e.one
let mul := e.mul
let inv := e.Inv
let div := e.div
let npow := e.pow ℕ
let zpow := e.pow ℤ
apply e.injective.commGroup _ <;> intros <;> exact e.apply_symm_apply _
