Theorems · Definition · nonassociative algebras

LieSubalgebra.toLieSubmodule

{R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (K : LieSubalgebra R L) → LieSubmodule R (↥K) L

Given a Lie subalgebra K ⊆ L, if we view L as a K-module by restriction, it contains a distinguished Lie submodule for the action of K, namely K itself.

Defined in

Mathlib.Algebra.Lie.Submodule

Cited by

26 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext

Assumes

CommRingLieRingLieAlgebra