Structures · Algebra
LieModule.IsNilpotent
A Lie module is nilpotent if its lower central series reaches 0 (in a finite number of steps).
- Defined in
- Mathlib.Algebra.Lie.Nilpotent
- Shape
- 2 explicit arguments · adds nilpotent_int
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- TensorProduct
How is a type an instance?
Loading the hierarchy index…
Assumed by26
- LieModule.IsNilpotent.nilpotent
- LieModule.exists_forall_pow_toEnd_eq_zero
- Function.Surjective.lieModuleIsNilpotent
- LieModule.nontrivial_lowerCentralSeriesLast
- LieModule.nontrivial_max_triv_of_isNilpotent
- LieModule.isNilpotent_of_le
- LieModule.zero_genWeightSpace_eq_top_of_nilpotent
- LieModule.isNilpotent_toEnd_of_isNilpotent
- LieModule.maxNilpotentSubmodule_eq_top_of_isNilpotent
- Function.Injective.lieModuleIsNilpotent
- LieModule.isTrivial_of_nilpotencyLength_le_one
- LieModule.lowerCentralSeriesLast_le_of_not_isTrivial
- LieModule.traceForm_eq_zero_of_isNilpotent
- LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff
- LieModule.isNilpotent_toEnd_of_isNilpotent₂
- LieModule.zero_genWeightSpace_eq_top_of_nilpotent'
- LieModule.nilpotencyLength_eq_zero_iff
- LieModule.posFittingCompOf_eq_bot_of_isNilpotent
- LieModule.maxGenEigenSpace_toEnd_eq_top
- LieModule.posFittingComp_eq_bot_of_isNilpotent
- LieIdeal.instIsNilpotentSubtypeMemOfIsNilpotent
- LieAlgebra.isSolvable_of_isNilpotent
- LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent
- LieModule.instIsNilpotentTensor
- LieModule.instIsNilpotentSup
- LieModule.IsNilpotent.nilpotent_int
Ancestors0
No ancestors.