coe_ringEquiv' — Mathlib

English

Let R be a CommSemiring and A1, A2 be semirings that are algebras over R. For any algebra equivalence e: A1 ≃ₐ[R] A2, the underlying ring equivalence agrees with e as a map; i.e., the action on elements is exactly the same whether viewed as a ring isomorphism or as the algebra equivalence.

Русский

Пусть R — коммутативное полукольцо, A1 и A2 — полукольца с алгебраическими структурами над R. Для любой алгебра эквивалентности e: A1 ≃ₐ[R] A2 совпадает отображение как кольцевое эквивалентность и как сама функция e на элементах.

LaTeX

$$$ (e^{\text{toRingEquiv}} : A_1 \to A_2) = e, $$$

Lean4

theorem coe_ringEquiv' : (e.toRingEquiv : A₁ → A₂) = e :=
  rfl

Похожие утверждения