symm

Mathlib.Logic.Function.Conjugate

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

English

If f commutes with g, then g commutes with f.

Русский

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

LaTeX

$$$ \text{Commute } f g \Rightarrow \text{Commute } g f $$$

Lean4

@[symm]
theorem symm (h : Commute f g) : Commute g f := fun x ↦ (h x).symm

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

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

Разделы

Аффилиация

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