comp_right

Mathlib.Logic.Function.Conjugate

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

/-- If `f` commutes with `g` and `g'`, then it commutes with `g ∘ g'`. -/
theorem comp_right (h : Commute f g) (h' : Commute f g') : Commute f (g ∘ g') :=
  Semiconj.comp_right h h'

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

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

Разделы

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

Аффилиация

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