id_monCat_comp — Mathlib

English

For any G in MonCat and H in MonCat, for f: G →* H, the composition of f with the identity on G is f: f ∘ id_G = f.

Русский

Для любого G в MonCat и H в MonCat, если f: G →* H, то композиция f с идентичностью на G равна f: f ∘ id_G = f.

LaTeX

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

Lean4

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

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