Theorems · Inductive type · nonassociative algebras
LeftPreLieAlgebra
(R : Type u_1) → [CommRing R] → (L : Type u_2) → [LeftPreLieRing L] → Type (max u_1 u_2)
A LeftPreLieAlgebra is a LeftPreLieRing with an action of a CommRing satisfying
r • x * y = r • (x * y) and x * (r • y) = r • (x * y).
- Defined in
- Mathlib.Algebra.NonAssoc.PreLie.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CommRingLeftPreLieRing
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.
- CommRingstatement · cited by 17,173
- LeftPreLieRingstatement · cited by 6
Cited by8
Results whose statement or proof uses this declaration.
- LeftPreLieAlgebra.extstatement and proof · cited by 1
- LeftPreLieAlgebra.ext_iffstatement and proof · cited by 0
- LeftPreLieAlgebra.noConfusionstatement and proof · cited by 0
- LeftPreLieAlgebra.noConfusionTypestatement and proof · cited by 0
- LeftPreLieAlgebra.mk.noConfusionstatement · cited by 0
- LeftPreLieAlgebra.recOnstatement and proof · cited by 0
- LeftPreLieAlgebra.casesOnstatement and proof · cited by 0
- LeftPreLieAlgebra.ctorIdxstatement and proof · cited by 0