toMulHom_injective

Mathlib.Algebra.Group.Hom.Defs

URI: https://scilib.ai/kg/mathlib#MonoidHom.toMulHom_injective

← MathLib Explorer

English

The map sending a MonoidHom to MulHom is injective.

Русский

Отображение моноидного гомоморфизма в MulHom инъективно.

LaTeX

$$Injective (MonoidHom.toMulHom)$$

Lean4

@[to_additive]
theorem toMulHom_injective [MulOne M] [MulOne N] : Function.Injective (MonoidHom.toMulHom : (M →* N) → M →ₙ* N) :=
  Function.Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru