Theorems · Inductive type · nonassociative algebras
LieRing
Type v → Type v
A Lie ring is an additive group with compatible product, known as the bracket, satisfying the Jacobi identity.
- Defined in
- Mathlib.Algebra.Lie.Basic
- Cited by
- 1,548 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by1,994
Results whose statement or proof uses this declaration.
- LieAlgebrastatement · cited by 1,246
- LieRingModulestatement · cited by 727
- LieSubmodulestatement · cited by 489
- LieModulestatement · cited by 424
- LieSubalgebrastatement · cited by 418
- LieHomstatement · cited by 382
- LieIdealstatement and proof · cited by 282
- LieRing.ofAssociativeRingstatement · cited by 227
- LieRing.IsNilpotentstatement and proof · cited by 176
- LieModule.Weightstatement · cited by 172
- LieSubmodule.toSubmodulestatement and proof · cited by 150
- LieModule.toEndstatement and proof · cited by 144
Showing the 200 most cited of 1,994.