conj_comp

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.conj_comp

English

Conjugation distributes over composition of functions: e.conj(f1 ∘ f2) = e.conj(f1) ∘ e.conj(f2).

Русский

Сопряжение распределяется по композиции функций: e.conj(f1 ∘ f2) = e.conj(f1) ∘ e.conj(f2).

LaTeX

$$$ e.conj (f_1 \circ f_2) = e.conj f_1 \circ e.conj f_2 $$$

Lean4

theorem conj_comp (e : α ≃ β) (f₁ f₂ : α → α) : e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂ := by apply arrowCongr_comp

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

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

Разделы

Аффилиация

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