English
Let e: α ≃ β be an equivalence and β a NonUnitalCommRing. Then α inherits a NonUnitalCommRing structure transported along e.
Русский
Пусть e: α ≃ β — эквивалентность и β — неполнокольцо с коммутативной умножением. Тогда α наследует структуру перенесённого через e NonUnitalCommRing.
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)$$$
Lean4
/-- Transfer `NonUnitalCommRing` across an `Equiv` -/
protected abbrev nonUnitalCommRing [NonUnitalCommRing β] : NonUnitalCommRing α :=
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.nonUnitalCommRing _ <;> intros <;> exact e.apply_symm_apply _
