Structures · Algebra
LieRingModule
A Lie ring module is an additive group, together with an additive action of a
Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms.
(For representations of Lie algebras see LieModule.)
- Defined in
- Mathlib.Algebra.Lie.Basic
- Shape
- 2 explicit arguments · adds add_lie, lie_add, leibniz_lie
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- TensorProduct
- Matrix
- Module.End
- Derivation
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by923
- LieSubmodule.toSubmodule
- LieModule.toEnd
- LieModule.genWeightSpace
- LieModule.lowerCentralSeries
- LieSubmodule.map
- LieModule.Weight.IsNonZero
- LieModule.Weight.toLinear
- LieModule.traceForm
- LieModule.toEnd_apply_apply
- LieModuleHom.toLinearMap
- LieSubmodule.toSubmodule_inj
- LieModule.Weight.IsZero
- LieModule.chainTopCoeff
- LieSubmodule.incl
- LieModule.lowerCentralSeries_succ
- LieModule.maxTrivSubmodule
- LieModule.Cohomology.twoCocycle
- LieSubmodule.lie_mem
- LieSubmodule.lieSpan
- LieModule.chainBotCoeff
- LieSubmodule.ucs
- LieSubmodule.comap
- LieSubmodule.normalizer
- add_lie
- LieModule.chainTop
- lie_smul
- lie_add
- lie_zero
- LieSubmodule.restr
- LieSubmodule.lieSpan_le
- LieModule.genWeightSpaceOf
- zero_lie
- LieDerivation.toLinearMap
- smul_lie
- LieSubmodule.lieIdeal_oper_eq_span
- LinearMap.BilinForm.lieInvariant
- LieModuleHom.range
- LieSubmodule.subset_lieSpan
- LieModule.posFittingComp
- LieModule.isNilpotent_iff
- LieSubmodule.Quotient.mk'
- LieSubmodule.lcs
- LieModule.Weight.genWeightSpace_ne_bot
- LieModuleEquiv.symm
- LieSubmodule.lieIdeal_oper_eq_linear_span'
- LieModule.genWeightSpace.congr_simp
- LieSubmodule.mem_bot
- LieModule.Weight.IsZero.eq
- LieModule.Weight.ker
- LieSubmodule.mem_toSubmodule