Structures · Algebra
LieModule.LinearWeights
A typeclass encoding the fact that a given Lie module has linear weights, vanishing on the derived ideal.
- Defined in
- Mathlib.Algebra.Lie.Weights.Linear
- Shape
- 3 explicit arguments · adds map_add, map_smul, map_lie
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
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 by26
- LieModule.Weight.toLinear
- LieModule.Weight.ker
- LieModule.Weight.toLinear_apply
- LieModule.Weight.coe_toLinear_eq_zero_iff
- LieModule.traceForm_eq_sum_finrank_nsmul
- LieModule.exists_forall_lie_eq_smul
- LieModule.traceForm_genWeightSpace_eq
- LieModule.Weight.coe_coe
- LieModule.shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply
- LieModule.range_traceForm_le_span_weight
- LieModule.shiftedGenWeightSpace.toEnd_eq
- LieModule.traceForm_eq_sum_finrank_nsmul'
- LieModule.LinearWeights.map_lie
- LieModule.traceForm_eq_sum_finrank_nsmul_mul
- LieModule.Weight.instCoeLinearMap
- LieModule.shiftedGenWeightSpace.instLieRingModuleSubtypeMemLieSubmodule
- LieModule.Weight.apply_lie
- LieModule.shiftedGenWeightSpace.instSubtypeMemLieSubmodule
- LieModule.Weight.ker.congr_simp
- LieModule.shiftedGenWeightSpace.instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian
- LieModule.Weight.coe_toLinear_ne_zero_iff
- LieModule.Weight.instLinearMapClass
- LieModule.exists_nontrivial_weightSpace_of_isNilpotent
- LieModule.LinearWeights.map_smul
- LieModule.Weight.toLinear.congr_simp
- LieModule.LinearWeights.map_add
Ancestors0
No ancestors.