Theorems · Definition · nonassociative algebras

LieAlgebra.loopAlgebra

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

A loop algebra is the base change of a Lie algebra L over R by R[z,z⁻¹]. We make a slightly more general definition which coincides with the Laurent polynomial construction when A = ℤ

Defined in

Mathlib.Algebra.Lie.Loop

Cited by

7 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLieRingLieAlgebra