English
Let e: α ≃ β. If β is a Group, then α becomes a Group under the transported multiplication and inverse/division operations.
Русский
Пусть e: α ≃ β. Если β имеется группа, то α становится группой с перенесённой операцией умножения и оборотом/делением.
LaTeX
$$$\text{Group}_\alpha \text{ with } a \star b := e^{-1}(e(a)\cdot e(b)), \ inv_\alpha(a) := e^{-1}(e(a)^{-1}), \ 1_\alpha := e^{-1}(1)$$$
Lean4
/-- Transfer `Group` across an `Equiv` -/
@[to_additive /-- Transfer `AddGroup` across an `Equiv` -/
]
protected abbrev group [Group β] : Group α := 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.group _ <;> intros <;> exact e.apply_symm_apply _
