comp_id_grp — Mathlib

English

Composition with the identity on the domain is neutral: for any G, monoid H and f: G →* H, f ∘ id_G = f.

Русский

Композиция с тождеством на области не меняет гомоморфизм: f ∘ id_G = f.

LaTeX

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

Lean4

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

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