Theorems · Definition · nonassociative algebras
LieAlgebra.Extension.incl
{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) → N →ₗ⁅R⁆ self.LThe inclusion homomorphism N →ₗ⁅R⁆ L
- Defined in
- Mathlib.Algebra.Lie.Extension
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
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 by11
Results whose statement or proof uses this declaration.
- LieAlgebra.Extension.toKerproof · cited by 8
- LieAlgebra.Extension.proj_surjectiveproof · cited by 4
- LieAlgebra.Extension.ringModuleOf_bracket_projproof · cited by 1
- LieAlgebra.Extension.incl_apply_mem_kerstatement and proof · cited by 1
- LieAlgebra.Extension.lie_toKer_applystatement · cited by 1
- LieAlgebra.Extension.proj_inclstatement · cited by 1
- LieAlgebra.Extension.IsExtensionstatement · cited by 0
- LieAlgebra.IsExtension.extension_inclstatement and proof · cited by 0
- LieAlgebra.Extension.incl_injectivestatement and proof · cited by 0
- LieAlgebra.Extension.lie_incl_mem_kerstatement and proof · cited by 0
- LieAlgebra.Extension.ofTwoCocycle_incl_applystatement · cited by 0