Theorems · Definition · nonassociative algebras

LieAlgebra.IsExtension.extension

{R : Type u_1} →
  {N : Type u_2} →
    {L : Type u_3} →
      {M : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : LieRing N] →
                [inst_4 : LieAlgebra R N] →
                  [inst_5 : LieRing M] →
                    [inst_6 : LieAlgebra R M] →
                      {i : N →ₗ⁅R⁆ L} → {p : L →ₗ⁅R⁆ M} → LieAlgebra.IsExtension i p → LieAlgebra.Extension R N M

The bundled LieAlgebra.Extension corresponding to LieAlgebra.IsExtension

Defined in

Mathlib.Algebra.Lie.Extension

Cited by

5 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebraLieRingLieAlgebra