Structures · Algebra
LieModule
A Lie module is a module over a commutative ring, together with a linear action of a Lie algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms.
- Defined in
- Mathlib.Algebra.Lie.Basic
- Shape
- 3 explicit arguments · adds smul_lie, lie_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- Int
How is a type an instance?
Loading the hierarchy index…
Assumed by518
- LieModule.toEnd
- LieModule.genWeightSpace
- LieModule.Weight.IsNonZero
- LieModule.Weight.toLinear
- LieModule.traceForm
- LieModule.toEnd_apply_apply
- LieModule.Weight.IsZero
- LieModule.chainTopCoeff
- LieModule.maxTrivSubmodule
- LieModule.Cohomology.twoCocycle
- LieModule.chainBotCoeff
- LieSubmodule.ucs
- LieSubmodule.normalizer
- LieModule.chainTop
- lie_smul
- LieModule.genWeightSpaceOf
- LieDerivation.toLinearMap
- smul_lie
- LieModule.posFittingComp
- LieModule.isNilpotent_iff
- LieSubmodule.Quotient.mk'
- LieModule.Weight.genWeightSpace_ne_bot
- LieSubmodule.lieIdeal_oper_eq_linear_span'
- LieModule.genWeightSpace.congr_simp
- LieModule.Weight.IsZero.eq
- LieModule.Weight.ker
- LieAlgebra.ofProd
- LieModule.Weight.toLinear_apply
- LieModule.posFittingCompOf
- LieModule.coe_chainTop
- LieModule.traceForm_comm
- LieSubmodule.ucs_succ
- LieModule.genWeightSpaceChain
- LieSubmodule.baseChange
- LieSubmodule.lieIdeal_oper_eq_linear_span
- LieModule.Cohomology.d₁₂
- LieModule.IsNilpotent.nilpotent
- LieModule.ker
- LieModule.rank
- LieModule.weightSpace
- LieModule.iSupIndep_genWeightSpace
- LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add
- LieModule.Weight.genWeightSpace_ne_bot'
- LieModule.traceForm_apply_apply
- LieSubmodule.idealizer
- LieModule.chainBot
- LieModule.shiftedGenWeightSpace
- LieAlgebra.rootSpaceWeightSpaceProduct
- LieModule.chainTopCoeff_zero
- LieModule.Cohomology.d₂₃
Ancestors0
No ancestors.