comp_left

Mathlib.Logic.Function.Conjugate

URI: https://scilib.ai/kg/mathlib#Function.Commute.comp_left

← MathLib Explorer

English

If f and f' commute with g, then f ∘ f' commutes with g.

Русский

Если f и f' коммутируют с g, то f ∘ f' коммутирует с g.

LaTeX

$$$ \text{Commute } (f \circ f') \; g $$$

Lean4

/-- If `f` and `f'` commute with `g`, then `f ∘ f'` commutes with `g` as well. -/
nonrec theorem comp_left (h : Commute f g) (h' : Commute f' g) : Commute (f ∘ f') g :=
  h.comp_left h'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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