Structures · Algebra
LieModule.IsTriangularizable
A Lie module M of a Lie algebra L is triangularizable if the endomorphism of M defined by
any x : L is triangularizable.
- Defined in
- Mathlib.Algebra.Lie.Weights.Basic
- Shape
- 3 explicit arguments · adds maxGenEigenspace_eq_top
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 by144
- LieAlgebra.IsKilling.rootSystem
- LieAlgebra.IsKilling.chainLength
- LieAlgebra.IsKilling.root_apply_coroot
- LieAlgebra.IsKilling.sl2SubmoduleOfRoot
- LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace
- LieAlgebra.IsKilling.invtSubmoduleToLieIdeal
- LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton
- LieAlgebra.IsKilling.coroot_eq_zero_iff
- LieAlgebra.IsKilling.finrank_rootSpace_eq_one
- LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff
- LieModule.Weight.IsNonZero.neg
- LieModule.Weight.coe_neg
- LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero
- LieModule.iSup_genWeightSpace_eq_top'
- LieModule.IsTriangularizable.maxGenEigenspace_eq_top
- LieAlgebra.IsKilling.apply_coroot_eq_cast'
- IsSl2Triple.h_eq_coroot
- LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg
- LieAlgebra.IsKilling.chainTopCoeff_zero_right
- LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero
- LieModule.iSup_genWeightSpace_eq_top
- LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace
- LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt
- LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup
- LieIdeal.rootSpan
- LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff
- LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg
- LieAlgebra.Basis.baseSupportEquiv
- LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff
- LieAlgebra.IsKilling.sl2SubalgebraOfRoot
- LieAlgebra.IsKilling.chainLength_of_isZero
- LieAlgebra.Basis.base
- LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_le
- LieAlgebra.IsKilling.chainLength_smul
- LieAlgebra.IsKilling.biSup_corootSpace_eq_top
- LieIdeal.root_apply_eq_zero_of_notMem_rootSet
- LieModule.Weight.IsZero.neg
- LieAlgebra.IsKilling.iInf_ker_weight_eq_bot
- LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule
- LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker
- LieIdeal.toInvtRootSubmodule
- LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal
- LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet
- LieModule.traceForm_eq_sum_finrank_nsmul
- LieAlgebra.IsKilling.span_weight_eq_top
- LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot
- LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux
- LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace
- LieAlgebra.IsKilling.reflectRoot
- LieIdeal.rootSpace_le_of_apply_coroot_ne_zero
Ancestors0
No ancestors.