conj_apply_apply

Mathlib.Algebra.Module.Equiv.Basic

URI: https://scilib.ai/kg/mathlib#LinearEquiv.conj_apply_apply

English

Conjugation respects composition: conj of a composition equals the composition of conjugates.

Русский

Сопряжение сохраняет композицию: conj(g ∘ f) = conj(g) ∘ conj(f).

LaTeX

$$$e.conj (g \circ f) = (e.conj g) \circ (e.conj f)$$$

Lean4

theorem conj_apply_apply (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁') (x : M₂') : e.conj f x = e (f (e.symm x)) :=
  rfl

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

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

Разделы

Аффилиация

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