Theorems · Definition · nonassociative algebras

LieAlgebra.Extension.mk.noConfusion

{R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_4} →
      {inst : CommRing R} →
        {inst_1 : LieRing N} →
          {inst_2 : LieAlgebra R N} →
            {inst_3 : LieRing M} →
              {inst_4 : LieAlgebra R M} →
                {P : Sort u} →
                  {L : Type u_5} →
                    {instLieRing : LieRing L} →
                      {instLieAlgebra : LieAlgebra R L} →
                        {incl : N →ₗ⁅R⁆ L} →
                          {proj : L →ₗ⁅R⁆ M} →
                            {IsExtension : LieAlgebra.IsExtension incl proj} →
                              {L' : Type u_5} →
                                {instLieRing' : LieRing L'} →
                                  {instLieAlgebra' : LieAlgebra R L'} →
                                    {incl' : N →ₗ⁅R⁆ L'} →
                                      {proj' : L' →ₗ⁅R⁆ M} →
                                        {IsExtension' : LieAlgebra.IsExtension incl' proj'} →
                                          { L := L, instLieRing := instLieRing, instLieAlgebra := instLieAlgebra,
                                                incl := incl, proj := proj, IsExtension := IsExtension } =
                                              { L := L', instLieRing := instLieRing', instLieAlgebra := instLieAlgebra',
                                                incl := incl', proj := proj', IsExtension := IsExtension' } →
                                            (L = L' →
                                                instLieRing ≍ instLieRing' →
                                                  instLieAlgebra ≍ instLieAlgebra' → incl ≍ incl' → proj ≍ proj' → P) →
                                              P

Defined in

Mathlib.Algebra.Lie.Extension

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms