English
Let e: α ≃ β be an equivalence and β a NonUnitalNonAssocRing. Then α inherits a NonUnitalNonAssocRing structure transported along e.
Русский
Пусть e: α ≃ β — эквивалентность, и β обладает структурой NonUnitalNonAssocRing. Тогда α наследует перенесённую через e структуру NonUnitalNonAssocRing.
LaTeX
$$$$(\alpha, 0_\alpha, +_\alpha, \cdot_\alpha, -_\alpha)$$ transported via $e$ with definitions $x +_\alpha y = e^{-1}(e x + e y)$, $x \cdot_\alpha y = e^{-1}(e x \cdot e y)$, $0_\alpha = e^{-1}(0)$, $-\_\alpha x = e^{-1}(- e x)$, yielding a NonUnitalNonAssocRing structure on $\alpha$.$$
Lean4
/-- Transfer `NonUnitalNonAssocRing` across an `Equiv` -/
protected abbrev nonUnitalNonAssocRing [NonUnitalNonAssocRing β] : NonUnitalNonAssocRing α :=
by
let zero := e.zero
let add := e.add
let mul := e.mul
let neg := e.Neg
let sub := e.sub
let nsmul := e.smul ℕ
let zsmul := e.smul ℤ
apply e.injective.nonUnitalNonAssocRing _ <;> intros <;> exact e.apply_symm_apply _
