English
Let e: α ≃ β be an equivalence and β a NonUnitalRing. Then α inherits a NonUnitalRing structure transported along e.
Русский
Пусть e: α ≃ β — эквивалентность и β — неединственное кольцо. Тогда α получает структуру NonUnitalRing, перенесённую через e.
LaTeX
$$$(\alpha, 0_\alpha, +_\alpha, \cdot_\alpha, -_\alpha)$ транспортируется через e; определения через $e^{-1}$ задают кольцообразную структуру на α.$$
Lean4
/-- Transfer `NonUnitalRing` across an `Equiv` -/
protected abbrev nonUnitalRing [NonUnitalRing β] : NonUnitalRing α :=
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.nonUnitalRing _ <;> intros <;> exact e.apply_symm_apply _
