Theorems · Definition · nonassociative algebras

LieAlgebra.ofTwoCocycle.mk.noConfusion

{R : Type u_5} →
  {L : Type u_6} →
    {M : Type u_7} →
      {inst : CommRing R} →
        {inst_1 : LieRing L} →
          {inst_2 : LieAlgebra R L} →
            {inst_3 : AddCommGroup M} →
              {inst_4 : Module R M} →
                {inst_5 : LieRingModule L M} →
                  {inst_6 : LieModule R L M} →
                    {c : ↥(LieModule.Cohomology.twoCocycle R L M)} →
                      {P : Sort u} →
                        {carrier carrier' : L × M} →
                          { carrier := carrier } = { carrier := carrier' } → (carrier ≍ carrier' → P) → P

Defined in

Mathlib.Algebra.Lie.Extension

Cited by

1 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Quot.sound