Theorems · Definition · nonassociative algebras

LieAlgebra.loopAlgebraEquivLaurent

(R : Type u_1) →
  (L : Type u_3) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] → LieAlgebra.loopAlgebra R ℤ L ≃ₗ⁅R⁆ TensorProduct R (LaurentPolynomial R) L

An Lie algebra isomorphism between the Loop algebra (with A = ℤ) and the tensor product with Laurent polynomials.

Defined in

Mathlib.Algebra.Lie.Loop

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebra