comp_id

Mathlib.Algebra.Order.Hom.Ring

URI: https://scilib.ai/kg/mathlib#OrderRingHom.comp_id

English

Composing with the identity on the right leaves the map unchanged: f ∘ id = f.

Русский

Сочетание с тождественной слева слева не изменяет отображение: f ∘ id = f.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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