Theorems · Inductive type · nonassociative algebras
LieAlgebra
(R : Type u) → (L : Type v) → [CommRing R] → [LieRing L] → Type (max u v)
A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.
- Defined in
- Mathlib.Algebra.Lie.Basic
- Cited by
- 1,246 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · 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.
Cited by1,589
Results whose statement or proof uses this declaration.
- LieModulestatement · cited by 424
- LieSubalgebrastatement · cited by 418
- LieHomstatement · cited by 382
- LieIdealstatement and proof · cited by 282
- LieModule.Weightstatement · cited by 172
- LieModule.toEndstatement and proof · cited by 144
- LieSubalgebra.IsCartanSubalgebrastatement · cited by 135
- LieModule.IsTriangularizablestatement · cited by 125
- LieAlgebra.IsKillingstatement · cited by 122
- LieModule.genWeightSpacestatement and proof · cited by 99
- LieDerivationstatement · cited by 95
- LieSubalgebra.toSubmodulestatement and proof · cited by 90
Showing the 200 most cited of 1,589.