comp_id_commMonCat — Mathlib

English

For MonoidHom f: G → H, the composition of identity on H with f is f: id_H ∘ f = f.

Русский

Для моноидного гомоморфизма f: G → H, композиция идентичности на H с f равна f.

LaTeX

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

Lean4

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

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