Structures · Algebra
LieAdmissibleRing
A LieAdmissibleRing is a NonUnitalNonAssocRing such that the canonical bracket
⁅x, y⁆ := x * y - y * x turns it into a LieRing. This is expressed by an associator identity.
- Shape
- One type argument · adds assoc_def
Extends1
Extended by2
Forgetful instances
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by4
Ancestors55
- 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
- LieAlgebra.IsSolvable
- LieRing
- Mul
- MulZeroClass
- NSMul
- Neg
- NegZeroClass
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- Nonempty
- OfNat
- One
- SMul
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero