id_grp_comp — Mathlib

English

Left identity law for composition with identity on the target: (id_H) ∘ f = f for f:G→*H.

Русский

Левый закон тождественности для композиции: id_H ∘ f = f.

LaTeX

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

Lean4

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

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