Structures · Algebra
LieRing
A Lie ring is an additive group with compatible product, known as the bracket, satisfying the Jacobi identity.
- Defined in
- Mathlib.Algebra.Lie.Basic
- Shape
- One type argument · adds add_lie, lie_add, lie_self, leibniz_lie
Extends2
Extended by1
Forgetful instances
Concrete types that are instances17
- TensorProduct
- DirectSum
- RestrictScalars
- Derivation
- CommutatorRing
- LieDerivation
- LeftInvariantDerivation
- LieAlgebra.ofTwoCocycle
- LieAlgebra.SemiDirectSum
- Matrix.ToLieAlgebra
- FreeLieAlgebra
- AddGroupLieAlgebra
- GroupLieAlgebra
- LieAlgebra.Extension.L
- Subtype
- Prod
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by1,992
- LieIdeal
- LieRing.IsNilpotent
- LieSubmodule.toSubmodule
- LieModule.toEnd
- LieModule.genWeightSpace
- LieSubalgebra.toSubmodule
- LieAlgebra.rootSpace
- LieHom.toLinearMap
- LieModule.lowerCentralSeries
- LieAlgebra.ad
- LieSubmodule.map
- LieIdeal.toLieSubalgebra
- LieModule.Weight.IsNonZero
- LieHom.range
- LieModule.Weight.toLinear
- LieModule.traceForm
- LieModule.toEnd_apply_apply
- LieModule.Cohomology.twoCochain
- LieHom.ker
- LieModuleHom.toLinearMap
- LieSubmodule.toSubmodule_inj
- killingForm
- LieAlgebra.IsKilling.coroot
- LieEquiv.symm
- LieSubalgebra.root
- LieIdeal.map
- LieSubalgebra.lieSpan
- LieModule.Weight.IsZero
- LieModule.chainTopCoeff
- LieAlgebra.derivedSeries
- LieSubmodule.incl
- LieAlgebra.derivedSeriesOfIdeal
- LieModule.lowerCentralSeries_succ
- LieSubalgebra.toLieSubmodule
- lie_skew
- LieModule.maxTrivSubmodule
- LieAlgebra.IsKilling.rootSystem
- LieModule.Cohomology.twoCocycle
- LieSubmodule.lie_mem
- LieAlgebra.center
- LieAlgebra.corootSpace
- LieSubmodule.lieSpan
- LieModule.chainBotCoeff
- LieSubmodule.ucs
- LieIdeal.comap
- LieAlgebra.Extension.L
- LieSubmodule.comap
- LieSubmodule.normalizer
- add_lie
- LieModule.chainTop
Ancestors46
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Bracket
- HAdd
- HSub
- HVAdd
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- LieAlgebra.IsSolvable
- NSMul
- Neg
- NegZeroClass
- Nonempty
- OfNat
- One
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero