toOneHom_injective — Mathlib

English

The map sending a monoid hom to its underlying OneHom is injective.

Русский

Отображение, переводящее гомоморфизм моноидов в соответствующий OneHom, инъективно.

LaTeX

$$Injective (MonoidHom.toOneHom)$$

Lean4

@[to_additive]
theorem toOneHom_injective [MulOne M] [MulOne N] : Function.Injective (MonoidHom.toOneHom : (M →* N) → OneHom M N) :=
  Function.Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

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