Structures · Algebra
RightPreLieRing
RightPreLieRings are NonUnitalNonAssocRings such that the associator is symmetric in the
last two variables.
- Defined in
- Mathlib.Algebra.NonAssoc.PreLie.Basic
- Shape
- One type argument · adds assoc_symm'
Extends1
Extended by0
Nothing extends this class yet.
Forgetful instances
Every RightPreLieRing is also a
Concrete types that are instances1
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by7
Ancestors56
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Bracket
- Distrib
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- LieAdmissibleRing
- LieAlgebra.IsSolvable
- LieRing
- Mul
- MulZeroClass
- NSMul
- Neg
- NegZeroClass
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- Nonempty
- OfNat
- One
- SMul
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero