comp_one

Mathlib.Algebra.Order.Hom.Monoid

URI: https://scilib.ai/kg/mathlib#OrderMonoidHom.comp_one

English

For any f, left-composing with the identity yields f: f.comp (1 : α →*o β) = 1.

Русский

Для любого f левая композиция с единицей возвращает f: f.comp (1 : α →*o β) = 1.

LaTeX

$$$ f.comp (1 : α \to*o β) = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem comp_one (f : β →*o γ) : f.comp (1 : α →*o β) = 1 :=
  ext fun _ => map_one f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru