Theorems · Theorem · nonassociative algebras

LieAlgebra.Extension.mk.inj

∀ {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} {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_1 : Type u_5} {instLieRing_1 : LieRing L_1}
  {instLieAlgebra_1 : LieAlgebra R L_1} {incl_1 : N →ₗ⁅R⁆ L_1} {proj_1 : L_1 →ₗ⁅R⁆ M}
  {IsExtension_1 : LieAlgebra.IsExtension incl_1 proj_1},
  { L := L, instLieRing := instLieRing, instLieAlgebra := instLieAlgebra, incl := incl, proj := proj,
        IsExtension := IsExtension } =
      { L := L_1, instLieRing := instLieRing_1, instLieAlgebra := instLieAlgebra_1, incl := incl_1, proj := proj_1,
        IsExtension := IsExtension_1 } →
    L = L_1 ∧ instLieRing ≍ instLieRing_1 ∧ instLieAlgebra ≍ instLieAlgebra_1 ∧ incl ≍ incl_1 ∧ proj ≍ proj_1

Defined in

Mathlib.Algebra.Lie.Extension

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms