coe_addMonoidHom_injective — Mathlib

English

The map sending an AlgHom to its underlying AddMonoidHom is injective: two AlgHoms that agree as AddMonoidHoms are equal.

Русский

Отображение из AlgHom в его AddMonoidHom-интерпретацию инъективно: если две AlgHom совпадают как AddMonoidHom, то они равны.

LaTeX

$$\$\\text{AlgHom}.coe\\_addMonoidHom\\_injective : (A \\to_ R B) \\to (A \\to^+ B)\$ is injective$$

Lean4

theorem coe_addMonoidHom_injective : Function.Injective ((↑) : (A →ₐ[R] B) → A →+ B) :=
  RingHom.coe_addMonoidHom_injective.comp coe_ringHom_injective

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