asHom_injective

Mathlib.Algebra.Category.Grp.Basic

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.asHom_injective

English

For AddCommGrpCat, the map asHom: G → AddCommGrpCat.of ℤ ⟶ G is injective.

Русский

Для AddCommGrpCat отображение asHom: G → AddCommGrpCat.of ℤ ⟶ G инъективно.

LaTeX

$$$$ \forall G:\mathrm{AddCommGrpCat},\; \mathrm{Injective}((\mathrm{asHom}\;G)). $$$$

Lean4

theorem asHom_injective {G : AddCommGrpCat.{0}} : Function.Injective (@asHom G) := fun h k w => by
  simpa using CategoryTheory.congr_fun w 1

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

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

Разделы

Аффилиация

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