instModuleSubtypeMemOfIsScalarTower

English

Under compatible scalar towers, a Lie subalgebra inherits the central scalar action from the ambient algebra.

Русский

При совместимой башне скаляров подалгебра наследует центральное действие скаляров от общей алгебры.

LaTeX

$$$\text{IsCentralScalar}(R_1,L')$ under the given tower.$$

Lean4

/-- A Lie subalgebra inherits module structures from `L`. -/
instance [SMul R₁ R] [Module R₁ L] [IsScalarTower R₁ R L] (L' : LieSubalgebra R L) : Module R₁ L' :=
  L'.toSubmodule.module'

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