Theorems · Definition · nonassociative algebras
LieHom.id
{R : Type u} → {L₁ : Type v} → [inst : CommRing R] → [inst_1 : LieRing L₁] → [inst_2 : LieAlgebra R L₁] → L₁ →ₗ⁅R⁆ L₁The identity map is a morphism of Lie algebras.
- Defined in
- Mathlib.Algebra.Lie.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses no axioms
- Assumes
- CommRingLieRingLieAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idproof · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- LinearMapproof · cited by 10,215
- LieRingstatement and proof · cited by 1,548
- LieAlgebrastatement and proof · cited by 1,246
- LinearMap.idproof · cited by 625
- LieHomstatement · cited by 382
Cited by14
Results whose statement or proof uses this declaration.
- LieModule.toEnd_module_endstatement · cited by 2
- LieModule.isNilpotent_of_leproof · cited by 1
- LieRinehartAlgebra.Hom.idproof · cited by 1
- LieHom.fst_comp_inlstatement · cited by 0
- LieHom.id_applystatement · cited by 0
- LieHom.id_compstatement · cited by 0
- LieHom.coe_idstatement · cited by 0
- LieHom.inl_eq_prodstatement · cited by 0
- LieHom.inr_eq_prodstatement · cited by 0
- LieHom.snd_comp_inrstatement · cited by 0
- LieHom.pair_fst_sndstatement · cited by 0
- LieHom.comp_idstatement · cited by 0