English
A field structure can be transported along an equivalence; if β is a field and e: α ≃ β, then α carries a field structure.
Русский
Структура поля может переноситься вдоль эквивалентности; если у β есть поле и есть e: α ≃ β, то α получает структуру поля.
LaTeX
$$$[Field\ \beta] \Rightarrow [Field\ \alpha]$ via $e$; the transported structure satisfies the field axioms via $e$.$$
Lean4
/-- Transfer `Field` across an `Equiv` -/
protected abbrev field [Field β] : Field α :=
by
let add_group_with_one := e.addGroupWithOne
let neg := e.Neg
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.field _ <;> intros <;> exact e.apply_symm_apply _
