symm_trans_apply

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.symm_trans_apply

English

Same as Trans Apply: for e1: M1 ≃SL[σ₁₂] M2 and e2: M2 ≃SL[σ₂₃] M3, (e1.trans e2) c = e2 (e1 c).

Русский

То же самое, что и Trans Apply: (e1.trans e2) c = e2 (e1 c).

LaTeX

$$$ (e_1 \\trans e_2)(c) = e_2(e_1(c)) $$$

Lean4

@[simp]
theorem symm_trans_apply (e₁ : M₂ ≃SL[σ₂₁] M₁) (e₂ : M₃ ≃SL[σ₃₂] M₂) (c : M₁) :
    (e₂.trans e₁).symm c = e₂.symm (e₁.symm c) :=
  rfl

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

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

Разделы

Аффилиация

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