coe_monoidHom_injective — Mathlib

English

The map from AlgHom to its underlying MonoidHom is injective: different AlgHoms give different monoid homomorphisms.

Русский

Отображение из AlgHom в его базовый моноид-гомоморфизм инъективно: разные AlgHom порождают разные моноид-гомоморфизмы.

LaTeX

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

Lean4

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

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