coe_fun_injective — Mathlib

English

There is a canonical CoeOut from AlgEquiv to RingEquiv, i.e., AlgEquiv can be viewed as ring equivalences.

Русский

Существует каноническое преобразование AlgEquiv к RingEquiv, то есть алгебровые эквивалентности можно рассматривать как кольцевые эквивалентности.

LaTeX

$$CoeOut (AlgEquiv R A B) (RingEquiv A B)$$

Lean4

theorem coe_fun_injective : @Function.Injective (A₁ ≃ₐ[R] A₂) (A₁ → A₂) fun e => (e : A₁ → A₂) :=
  DFunLike.coe_injective

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