Theorems · Definition · nonassociative algebras

LieModule.toEnd

(R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → [LieModule R L M] → L →ₗ⁅R⁆ Module.End R M

A Lie module yields a Lie algebra morphism into the linear endomorphisms of the module. See also LieModule.toModuleHom.

Defined in

Mathlib.Algebra.Lie.OfAssociative

Cited by

144 results in Mathlib

Foundations

Depth 47 from the axioms, rests on 781 definitions · uses propext, Quot.sound

Assumes

CommRingLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModule