Theorems · Definition · nonassociative algebras

LieModuleEquiv.ofTop

(R : Type u) →
  (L : Type v) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        (M : Type u_1) → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → ↥⊤ ≃ₗ⁅R,L⁆ M

The natural equivalence between the 'top' Lie submodule and the enclosing Lie module.

Defined in

Mathlib.Algebra.Lie.Submodule

Cited by

2 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Quot.sound

Assumes

CommRingLieRingAddCommGroupModuleLieRingModule