trans — Mathlib

English

The composition of two Lie module equivalences e1 and e2 acts as e2 after e1 on any m.

Русский

Составление двух эквивалентностей Ли-модуля действует как e2 после e1 на любом элементе m.

LaTeX

$$$(e_1.Trans e_2) m = e_2(e_1 m)$$$

Lean4

/-- Lie module equivalences are transitive. -/
@[trans]
def trans (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) : M ≃ₗ⁅R,L⁆ P :=
  { LieModuleHom.comp e₂.toLieModuleHom e₁.toLieModuleHom, LinearEquiv.trans e₁.toLinearEquiv e₂.toLinearEquiv with }

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