English
Let e: α ≃ β be an equivalence and β a NonAssocRing. Then α inherits a NonAssocRing structure transported along e.
Русский
Пусть e: α ≃ β — эквивалентность и β — неполнокольцо. Тогда α получает перенесённую через e структуру NonAssocRing.
LaTeX
$$$(\alpha, +_\alpha, \cdot_\alpha) \text{ with } x +_\alpha y = e^{-1}(e x + e y),\; x \cdot_\alpha y = e^{-1}(e x \cdot e y)$; транспортировка по e задаёт NonAssocRing на α.$$
Lean4
/-- Transfer `NonAssocRing` across an `Equiv` -/
protected abbrev nonAssocRing [NonAssocRing β] : NonAssocRing α :=
by
let add_group_with_one := e.addGroupWithOne
let mul := e.mul
apply e.injective.nonAssocRing _ <;> intros <;> exact e.apply_symm_apply _
