comp_id — Mathlib

English

For any order-preserving monoid homomorphism f, composing with the identity on the left yields f: (OrderMonoidHom.id α).comp f = f.

Русский

Для любого упорядоченного моноид-гомоморфизма f композиция слева с единицей равна f: (OrderMonoidHom.id α).comp f = f.

LaTeX

$$$ (\mathrm{id}_{\alpha} \circ f) = f $$$

Lean4

@[to_additive (attr := simp)]
theorem comp_id (f : α →*o β) : f.comp (OrderMonoidHom.id α) = f :=
  rfl

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