English
A division ring structure can be transported along an equivalence; if β has a division ring structure and e: α ≃ β, then α does too.
Русский
Кольцо делимости можно перенести вдоль эквивалентности; если у β есть структура делимого кольца и e: α ≃ β, то и у α она есть.
LaTeX
$$$[DivisionRing\ β] \Rightarrow [DivisionRing\ α]$ via $e$; i.e., the transported structure makes the diagram commute with the inclusion.$$
Lean4
/-- Transfer `DivisionRing` across an `Equiv` -/
protected abbrev divisionRing [DivisionRing β] : DivisionRing α :=
by
let add_group_with_one := e.addGroupWithOne
let inv := e.Inv
let div := e.div
let mul := e.mul
let npow := e.pow ℕ
let zpow := e.pow ℤ
let nnratCast := e.nnratCast
let ratCast := e.ratCast
let nnqsmul := e.smul ℚ≥0
let qsmul := e.smul ℚ
apply e.injective.divisionRing _ <;> intros <;> exact e.apply_symm_apply _
