id_commGrp_comp

Mathlib.Algebra.Category.Grp.Basic

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

← MathLib Explorer

English

Right identity law for generators: id_H ∘ f = f.

Русский

Правый закон идентичности: id_H ∘ f = f.

LaTeX

$$$\mathrm{id}_H \circ f = f$$$

Lean4

@[to_additive (attr := deprecated "Proven by `simp only [CommGrpCat.hom_id, id_comp]`" (since := "2025-01-28"))]
theorem id_commGrp_comp {G : Type u} [Monoid G] {H : CommGrpCat.{u}} (f : G →* H) :
    MonoidHom.comp (CommGrpCat.Hom.hom (𝟙 H)) f = f := by simp

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

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

Разделы

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

Аффилиация

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