Structures · Algebra
LieAlgebra
A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.
- Defined in
- Mathlib.Algebra.Lie.Basic
- Shape
- 2 explicit arguments · adds lie_smul
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Int
How is a type an instance?
Loading the hierarchy index…
Assumed by1,593
- LieIdeal
- LieModule.toEnd
- LieModule.genWeightSpace
- LieSubalgebra.toSubmodule
- LieAlgebra.rootSpace
- LieHom.toLinearMap
- LieModule.lowerCentralSeries
- LieAlgebra.ad
- LieIdeal.toLieSubalgebra
- LieModule.Weight.IsNonZero
- LieHom.range
- LieModule.Weight.toLinear
- LieModule.traceForm
- LieModule.toEnd_apply_apply
- LieModule.Cohomology.twoCochain
- LieHom.ker
- killingForm
- LieAlgebra.IsKilling.coroot
- LieEquiv.symm
- LieSubalgebra.root
- LieIdeal.map
- LieSubalgebra.lieSpan
- LieModule.Weight.IsZero
- LieModule.chainTopCoeff
- LieAlgebra.derivedSeries
- LieAlgebra.derivedSeriesOfIdeal
- LieModule.lowerCentralSeries_succ
- LieSubalgebra.toLieSubmodule
- LieModule.maxTrivSubmodule
- LieAlgebra.IsKilling.rootSystem
- LieModule.Cohomology.twoCocycle
- LieAlgebra.center
- LieAlgebra.corootSpace
- LieModule.chainBotCoeff
- LieSubmodule.ucs
- LieIdeal.comap
- LieAlgebra.Extension.L
- LieSubmodule.normalizer
- LieModule.chainTop
- lie_smul
- LieAlgebra.Extension.proj
- LieSubalgebra.subset_lieSpan
- LieDerivation.ad
- LieHom.comp
- LieSubalgebra.normalizer
- LieHom.map_lie
- LieSubmodule.restr
- LieIdeal.incl
- LieAlgebra.Basis.h
- LieHom.idealRange