coe_ringEquiv_injective — Mathlib

English

Let e1, e2 be algebra isomorphisms A1 ≃ₐ[R] A2. If their underlying ring isomorphisms are the same, then e1 = e2. In other words, the map sending an algebra equivalence to its underlying ring equivalence is injective.

Русский

Пусть e1, e2 — алгебраические эквивалентности A1 ≃ₐ[R] A2. Если их основания кольцевые эквивалентности совпадают, то e1 = e2.

LaTeX

$$$\forall e_1,e_2:\ A_1 \simeq_{R} A_2,\ (e_1^{\text{ring}} = e_2^{\text{ring}}) \Rightarrow e_1 = e_2$$$

Lean4

theorem coe_ringEquiv_injective : Function.Injective ((↑) : (A₁ ≃ₐ[R] A₂) → A₁ ≃+* A₂) := fun _ _ h =>
  ext <| RingEquiv.congr_fun h

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