Theorems · Inductive type · nonassociative algebras
RightPreLieAlgebra
(R : Type u_1) → [CommRing R] → (L : Type u_2) → [RightPreLieRing L] → Type (max u_1 u_2)
A RightPreLieAlgebra is a RightPreLieRing 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
- CommRingRightPreLieRing
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
- RightPreLieRingstatement · cited by 6
Cited by8
Results whose statement or proof uses this declaration.
- RightPreLieAlgebra.extstatement and proof · cited by 1
- RightPreLieAlgebra.mk.noConfusionstatement · cited by 0
- RightPreLieAlgebra.casesOnstatement and proof · cited by 0
- RightPreLieAlgebra.ctorIdxstatement and proof · cited by 0
- RightPreLieAlgebra.ext_iffstatement and proof · cited by 0
- RightPreLieAlgebra.noConfusionstatement and proof · cited by 0
- RightPreLieAlgebra.noConfusionTypestatement and proof · cited by 0
- RightPreLieAlgebra.recOnstatement and proof · cited by 0