Theorems · Definition · nonassociative algebras

LieAlgebra.Extension.proj

{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] → (self : LieAlgebra.Extension R N M) → self.L →ₗ⁅R⁆ M

The projection homomorphism L →ₗ⁅R⁆ M

Defined in: Mathlib.Algebra.Lie.Extension
Cited by: 19 results in Mathlib
Foundations: Depth 6 from the axioms · uses no axioms
Assumes: CommRing LieRing LieAlgebra LieRing LieAlgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
LieRingstatement and proof · cited by 1,548
LieAlgebrastatement and proof · cited by 1,246
LieHomstatement · cited by 382
LieAlgebra.Extension.Lstatement · cited by 21
LieAlgebra.Extensionstatement and proof · cited by 20

Cited by22

Results whose statement or proof uses this declaration.

LieAlgebra.Extension.toKerstatement and proof · cited by 8
LieAlgebra.Extension.proj_surjectivestatement and proof · cited by 4
LieAlgebra.Extension.twoCocycleOfstatement and proof · cited by 3
LieAlgebra.Extension.lieModuleOfproof · cited by 3
LieAlgebra.Extension.oneCochainOfTwoSplittingstatement and proof · cited by 3
LieAlgebra.Extension.ringModuleOf_bracketstatement · cited by 2
LieAlgebra.Extension.ringModuleOf_bracket_projstatement and proof · cited by 1
LieAlgebra.Extension.twoCocycleOf_coe_coestatement and proof · cited by 1
LieAlgebra.Extension.incl_apply_mem_kerstatement and proof · cited by 1
LieAlgebra.Extension.oneCochainOfTwoSplitting_applystatement and proof · cited by 1
LieAlgebra.Extension.lie_toKer_applystatement · cited by 1
LieAlgebra.Extension.proj_inclstatement · cited by 1