trans_apply

Mathlib.Topology.Algebra.Module.Equiv

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

English

If e1: M1 ≃SL[σ₁₂] M2 and e2: M2 ≃SL[σ₂₃] M3, then for any c ∈ M1, (e1.trans e2)(c) = e2(e1(c)).

Русский

Если e1: M1 ≃SL[σ₁₂] M2 и e2: M2 ≃SL[σ₂₃] M3, то для любого c ∈ M1, (e1.trans e2)(c) = e2(e1(c)).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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