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