Theorems · Inductive type · nonassociative algebras

LieHom

(R : Type u_1) →
  (L : Type u_2) →
    (L' : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] → [LieAlgebra R L] → [inst_3 : LieRing L'] → [LieAlgebra R L'] → Type (max u_2 u_3)

A morphism of Lie algebras (denoted as L₁ →ₗ⁅R⁆ L₂) is a linear map respecting the bracket operations.

Defined in

Mathlib.Algebra.Lie.Basic

Cited by

382 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebra