instIsCentralScalarSubtypeMem — Mathlib

English

Subtypes of Lie subalgebras inherit a scalar tower structure from the ambient algebra.

Русский

Подтипы подалгебр Ли наследуют структуру башни скаляров от окружающей алгебры.

LaTeX

$$$\text{IsScalarTower}(R_1,R,L')(\text{L'})$$$

Lean4

instance [SMul R₁ R] [SMul R₁ᵐᵒᵖ R] [Module R₁ L] [Module R₁ᵐᵒᵖ L] [IsScalarTower R₁ R L] [IsScalarTower R₁ᵐᵒᵖ R L]
    [IsCentralScalar R₁ L] (L' : LieSubalgebra R L) : IsCentralScalar R₁ L' :=
  L'.toSubmodule.isCentralScalar

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