English
An equivalence e : α ≃ β induces a ring equivalence α ≃+* β, where the ring structure on α is transported back along e from β.
Русский
Любое эквивалентность e : α ≃ β порождает кольцевую эквивалентность α ≃+* β, причем структура кольца на α получается путём переноса структуры кольца на β обратно по e.
LaTeX
$$$\text{If } e: \alpha \simeq \beta, \text{ then } \alpha \cong_{\mathrm{ring}} \beta \text{ via transport along } e.$$$
Lean4
/-- An equivalence `e : α ≃ β` gives a ring equivalence `α ≃+* β`
where the ring structure on `α` is
the one obtained by transporting a ring structure on `β` back along `e`.
-/
def ringEquiv (e : α ≃ β) [Add β] [Mul β] : by
let add := Equiv.add e
let mul := Equiv.mul e
exact α ≃+* β := by
intros
exact
{ e with
map_add' := fun x y => by simp [add_def]
map_mul' := fun x y => by simp [mul_def] }
