Theorems · Definition · nonassociative algebras
LieRing.ofAssociativeRing
{A : Type v} → [Ring A] → LieRing AAn associative ring gives rise to a Lie ring by taking the bracket to be the ring commutator.
- Defined in
- Mathlib.Algebra.Lie.OfAssociative
- Cited by
- 227 results in Mathlib
- Foundations
- Depth 40 from the axioms, rests on 547 definitions · uses propext, Quot.sound
- Assumes
- Ring
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 by274
Results whose statement or proof uses this declaration.
- LieModule.toEndstatement · cited by 144
- LieAlgebra.adstatement · cited by 49
- LieModule.toEnd_apply_applystatement · cited by 39
- RootPairing.GeckConstruction.lieAlgebrastatement · cited by 14
- AlgHom.toLieHomstatement · cited by 8
- UniversalEnvelopingAlgebra.ιstatement · cited by 8
- LieAlgebra.SpecialLinear.slstatement · cited by 8
- LieAlgebra.IsKilling.coe_corootSpace_eq_span_singletonstatement · cited by 7
- UniversalEnvelopingAlgebra.liftstatement · cited by 7
- LieModule.traceForm_apply_applystatement · cited by 6
- RootPairing.GeckConstruction.cartanSubalgebrastatement · cited by 5
- RootPairing.GeckConstruction.cartanSubalgebra'statement · cited by 5
Showing the 200 most cited of 274.