Theorems · Inductive type · nonassociative algebras

LieModuleEquiv

(R : Type u) →
  (L : Type v) →
    (M : Type w) →
      (N : Type w₁) →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [Module R M] → [Module R N] → [LieRingModule L M] → [LieRingModule L N] → Type (max w w₁)

An equivalence of Lie algebra modules (denoted as M ≃ₗ⁅R,L⁆ N) is a linear equivalence which is also a morphism of Lie algebra modules.

Defined in

Mathlib.Algebra.Lie.Basic

Cited by

40 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingLieRingAddCommGroupAddCommGroupModuleModuleLieRingModuleLieRingModule