Theorems · Definition · nonassociative algebras
IsLieAbelian
(L : Type v) → [Bracket L L] → [Zero L] → Prop
A Lie algebra is Abelian iff it is trivial as a Lie module over itself.
- Defined in
- Mathlib.Algebra.Lie.Abelian
- Cited by
- 55 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LieModule.IsTrivialproof · cited by 14
- Bracketstatement and proof · cited by 8
Cited by64
Results whose statement or proof uses this declaration.
- LieAlgebra.Basis.isLieAbelian_cartanstatement and proof · cited by 7
- LieAlgebra.Extension.ringModuleOfstatement and proof · cited by 7
- LieAlgebra.Basis.isCartanSubalgebraproof · cited by 6
- LieAlgebra.Basis.iSupIndep_rootSpaceproof · cited by 3
- LieAlgebra.Extension.lieModuleOfstatement and proof · cited by 3
- LieAlgebra.Extension.ofTwoCocyclestatement and proof · cited by 3
- LieAlgebra.Extension.twoCocycleOfstatement and proof · cited by 3
- LieAlgebra.InvariantForm.orthogonal_disjointstatement and proof · cited by 3
- LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodulestatement and proof · cited by 3
- LieSubmodule.lie_abelian_iff_lie_self_eq_botstatement and proof · cited by 3
- Function.Injective.isLieAbelianstatement and proof · cited by 2
- LieAlgebra.IsSimple.non_abelianstatement · cited by 2