Basis

📁 Source: Mathlib/Algebra/Lie/Basis.lean

Statistics

Metric	Count
Definitions A, base, baseSupp, baseSupp', baseSupportEquiv, borelLower, borelUpper, cartan, e, f, h, h'	12
Theorems A_diag_eq_two, baseSupp_apply_h', baseSupp_apply_smul_e, baseSupp_apply_smul_f, borelLower_eq, borelLower_le_biSup, borelUpper_eq, borelUpper_le_biSup, cartanMatrix_base_eq, cartan_eq, cartan_eq_lieSpan, coe_baseSupportEquiv_apply, coe_cartan_eq_span, coe_linearMap_baseSupp', coroot_eq_h', ext, ext_iff, iSupIndep_rootSpace, iSup_cartan_borelLower_borelUpper_eq_top, instIsCartanSubalgebraCartanOfIsNoetherian, instIsLieAbelianSubtypeMemLieSubalgebraCartan, lie_e_f_ne, lie_h_e, lie_h_f, lie_h_h, linInd, linearIndepOn_root_baseSupp, linearIndependent_baseSupp, nondegen, root_mem_or_mem_neg, sl2, span_ef, symm_A, symm_baseSupp, symm_cartan, symm_e, symm_f, symm_h, symm_h', symm_symm	40
Total	52

LieAlgebra.Basis

Definitions

Name	Category	Theorems
A 📖	CompOp	9 math math: nondegen, lie_h_f, ext_iff, RootPairing.GeckConstruction.basis_A_eq, symm_A, A_diag_eq_two, cartanMatrix_base_eq, lie_h_e, baseSupp_apply_h'
base 📖	CompOp	3 math math: coroot_eq_h', cartanMatrix_base_eq, coe_baseSupportEquiv_apply
baseSupp 📖	CompOp	12 math math: borelLower_le_biSup, borelUpper_eq, symm_baseSupp, baseSupp_apply_smul_f, iSupIndep_rootSpace, baseSupp_apply_smul_e, borelUpper_le_biSup, borelLower_eq, coe_linearMap_baseSupp', coe_baseSupportEquiv_apply, linearIndependent_baseSupp, baseSupp_apply_h'
baseSupp' 📖	CompOp	3 math math: linearIndepOn_root_baseSupp, root_mem_or_mem_neg, coe_linearMap_baseSupp'
baseSupportEquiv 📖	CompOp	3 math math: coroot_eq_h', cartanMatrix_base_eq, coe_baseSupportEquiv_apply
borelLower 📖	CompOp	3 math math: borelLower_le_biSup, borelLower_eq, iSup_cartan_borelLower_borelUpper_eq_top
borelUpper 📖	CompOp	3 math math: borelUpper_eq, borelUpper_le_biSup, iSup_cartan_borelLower_borelUpper_eq_top
cartan 📖	CompOp	25 math math: borelLower_le_biSup, symm_h', cartan_eq, borelUpper_eq, linearIndepOn_root_baseSupp, coroot_eq_h', instIsCartanSubalgebraCartanOfIsNoetherian, symm_baseSupp, coe_cartan_eq_span, baseSupp_apply_smul_f, instIsLieAbelianSubtypeMemLieSubalgebraCartan, iSupIndep_rootSpace, ext_iff, baseSupp_apply_smul_e, cartanMatrix_base_eq, borelUpper_le_biSup, borelLower_eq, root_mem_or_mem_neg, coe_linearMap_baseSupp', cartan_eq_lieSpan, iSup_cartan_borelLower_borelUpper_eq_top, coe_baseSupportEquiv_apply, linearIndependent_baseSupp, symm_cartan, baseSupp_apply_h'
e 📖	CompOp	8 math math: symm_e, ext_iff, baseSupp_apply_smul_e, span_ef, symm_f, lie_e_f_ne, lie_h_e, sl2
f 📖	CompOp	8 math math: symm_e, lie_h_f, baseSupp_apply_smul_f, ext_iff, span_ef, symm_f, lie_e_f_ne, sl2
h 📖	CompOp	9 math math: lie_h_f, coe_cartan_eq_span, ext_iff, lie_h_h, lie_h_e, symm_h, sl2, cartan_eq_lieSpan, linInd
h' 📖	CompOp	3 math math: symm_h', coroot_eq_h', baseSupp_apply_h'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
A_diag_eq_two 📖	mathematical	—	A	—	IsAddTorsionFree.to_noZeroSMulDivisors_int sub_smul Nat.instAtLeastTwoHAddOfNat ofNat_smul_eq_nsmul IsSl2Triple.lie_h_e_nsmul sl2 lie_h_e Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg zero_add Mathlib.Tactic.Abel.zero_termg sub_eq_zero IsAddTorsionFree.zsmul_eq_zero_iff_left IsSl2Triple.e_ne_zero
baseSupp_apply_h' 📖	mathematical	—	DFunLike.coe Module.Dual LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id baseSupp h' AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing A	—	IsScalarTower.left linInd coe_cartan_eq_span LinearMap.coe_sum Finset.sum_apply RingHomInvPair.ids Module.Basis.span_repr_eq_single Submodule.subset_span Set.mem_range_self Finsupp.single_apply smul_ite zsmul_eq_mul mul_one smul_zero Finset.sum_congr Finset.sum_ite_eq
baseSupp_apply_smul_e 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid LieAlgebra.toModule DFunLike.coe Module.Dual LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id baseSupp e Bracket.bracket LieSubalgebra.instBracketSubtypeMem lieRingSelfModule	—	IsScalarTower.left coe_cartan_eq_span LieSubalgebra.mem_toSubmodule Submodule.span_induction baseSupp_apply_h' Int.cast_smul_eq_zsmul lie_h_e AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass zero_smul zero_lie AddSubmonoidClass.toAddMemClass AddMemClass.add_mem map_add SemilinearMapClass.toAddHomClass add_smul add_lie LieSubalgebra.instSMulMemClass SMulMemClass.smul_mem map_smul SemilinearMapClass.toMulActionSemiHomClass smul_assoc smul_lie lieAlgebraSelfModule
baseSupp_apply_smul_f 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid LieAlgebra.toModule DFunLike.coe Module.Dual LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id baseSupp f NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Bracket.bracket LieSubalgebra.instBracketSubtypeMem lieRingSelfModule	—	IsScalarTower.left neg_eq_iff_eq_neg neg_smul LinearMap.neg_apply baseSupp_apply_smul_e symm_baseSupp
borelLower_eq 📖	mathematical	—	borelLower iSup LieSubmodule LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubmodule.instSupSet Pi.instZero MulZeroClass.toZero Nat.instMulZeroClass LieAlgebra.rootSpace LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ AddMonoid.toNSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Pi.instNeg LinearMap.instNeg LieRing.ofAssociativeRing baseSupp	—	LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan IsScalarTower.left iSupIndep.le_iff_eq_of_iSup_eq_top LieSubmodule.instIsModularLattice iSupIndep_rootSpace iSup_cartan_borelLower_borelUpper_eq_top
borelLower_le_biSup 📖	mathematical	—	LieSubmodule LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder borelLower iSup LieSubmodule.instSupSet Pi.instZero MulZeroClass.toZero Nat.instMulZeroClass LieAlgebra.rootSpace LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ AddMonoid.toNSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Pi.instNeg LinearMap.instNeg LieRing.ofAssociativeRing baseSupp	—	LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan IsScalarTower.left iSup_congr_Prop LieAlgebra.rootSpace.congr_simp Finset.sum_congr symm_baseSupp borelUpper_le_biSup
borelUpper_eq 📖	mathematical	—	borelUpper iSup LieSubmodule LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubmodule.instSupSet Pi.instZero MulZeroClass.toZero Nat.instMulZeroClass LieAlgebra.rootSpace LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ AddMonoid.toNSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id baseSupp	—	LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan IsScalarTower.left iSupIndep.le_iff_eq_of_iSup_eq_top LieSubmodule.instIsModularLattice iSupIndep_rootSpace iSup_cartan_borelLower_borelUpper_eq_top
borelUpper_le_biSup 📖	mathematical	—	LieSubmodule LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder borelUpper iSup LieSubmodule.instSupSet Pi.instZero MulZeroClass.toZero Nat.instMulZeroClass LieAlgebra.rootSpace LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ AddMonoid.toNSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id baseSupp	—	LieSubalgebra.lieSpan_induction LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan IsScalarTower.left LieSubmodule.mem_iSup_of_mem smulCommClass_self lieAlgebraSelfModule iSup_congr_Prop LieAlgebra.rootSpace.congr_simp Finset.sum_congr nsmul_eq_mul iSup_pos Finset.sum_apply Pi.single_apply Nat.cast_ite Nat.cast_one CharP.cast_eq_zero CharP.ofCharZero ite_mul one_mul MulZeroClass.zero_mul Finset.sum_ite_eq' pow_one baseSupp_apply_smul_e sub_self AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SMulMemClass.smul_mem LieSubmodule.instSMulMemClass Unique.instSubsingleton Pi.instCanonicallyOrderedAddForall Nat.instCanonicallyOrderedAdd LinearMap.coe_sum add_smul Finset.sum_add_distrib LinearIndependent.restrict_scalars' Algebra.to_smulCommClass AddCommMonoid.nat_isScalarTower instFaithfulSMulNatOfCharZero IsScalarTower.right linearIndependent_baseSupp Fintype.linearIndependent_iffₛ LinearMap.ext iSup_subtype' Equiv.iSup_comp LieSubalgebra.lieModule LieAlgebra.mem_biSup_genWeightSpace_of
cartanMatrix_base_eq 📖	mathematical	—	RootPairing.Base.cartanMatrix LieModule.Weight LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike cartan Finite.of_fintype LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain Field.toSemifield instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule Ring.toSemiring instIsSimpleModule Finset Finset.instSetLike LieSubalgebra.root Module.Dual DivisionSemiring.toSemiring LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid LinearMap.addCommGroup RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass LieAlgebra.IsKilling.rootSystem base LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem DFunLike.coe Equiv Matrix RootPairing.Base.support EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex baseSupportEquiv A	—	Finite.of_fintype LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule IsScalarTower.left Algebra.to_smulCommClass LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem Matrix.ext FaithfulSMul.algebraMap_injective instFaithfulSMulIntOfCharZero Matrix.reindex_apply Matrix.submatrix_apply RootPairing.Base.algebraMap_cartanMatrixIn_apply coroot_eq_h' baseSupp_apply_h' eq_intCast RingHom.instRingHomClass Equiv.symm_apply_eq
cartan_eq 📖	mathematical	—	LieSubalgebra.toLieSubmodule cartan LieAlgebra.rootSpace LieModule.trivialIsNilpotent LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieRing.toAddCommGroup lieRingSelfModule instIsLieAbelianSubtypeMemLieSubalgebraCartan Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan IsScalarTower.left iSupIndep.le_iff_eq_of_iSup_eq_top LieSubmodule.instIsModularLattice iSupIndep_rootSpace iSup_cartan_borelLower_borelUpper_eq_top
cartan_eq_lieSpan 📖	mathematical	—	cartan LieSubalgebra.lieSpan Set.range h	—	—
coe_baseSupportEquiv_apply 📖	mathematical	—	LieModule.Weight.toLinear LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike cartan Finite.of_fintype LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain Field.toSemifield instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule Ring.toSemiring instIsSimpleModule LieModule.instLinearWeightsOfCharZero instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Ring.toAddCommGroup Module.free_of_finite_type_torsion_free' LieModule.Weight Finset Finset.instSetLike LieSubalgebra.root RootPairing.Base.support Module.Dual DivisionSemiring.toSemiring LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid LinearMap.addCommGroup RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass LieAlgebra.IsKilling.rootSystem base DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike baseSupportEquiv baseSupp	—	Finite.of_fintype LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieModule.instLinearWeightsOfCharZero instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Module.free_of_finite_type_torsion_free' IsScalarTower.left Algebra.to_smulCommClass
coe_cartan_eq_span 📖	mathematical	—	LieSubalgebra.toSubmodule cartan Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Set.range h	—	cartan_eq_lieSpan LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero lie_h_h
coe_linearMap_baseSupp' 📖	mathematical	—	LieModule.Weight.toLinear LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike cartan Finite.of_fintype LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain Field.toSemifield instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule Ring.toSemiring instIsSimpleModule LieModule.instLinearWeightsOfCharZero instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Ring.toAddCommGroup Module.free_of_finite_type_torsion_free' LieModule.Weight Finset Finset.instSetLike LieSubalgebra.root baseSupp' baseSupp	—	Finite.of_fintype LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieModule.instLinearWeightsOfCharZero instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Module.free_of_finite_type_torsion_free'
coroot_eq_h' 📖	mathematical	—	LieAlgebra.IsKilling.coroot cartan Finite.of_fintype EuclideanDomain.toCommRing Field.toEuclideanDomain instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain Field.toSemifield instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommSemiring.toSemiring CommRing.toCommSemiring LieRing.toAddCommGroup LieAlgebra.toModule GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule Ring.toSemiring instIsSimpleModule LieModule.Weight LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra Finset Finset.instSetLike LieSubalgebra.root RootPairing.Base.support Module.Dual DivisionSemiring.toSemiring LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid LinearMap.addCommGroup RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass LieAlgebra.IsKilling.rootSystem base DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike baseSupportEquiv h'	—	Finite.of_fintype LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieModule.instLinearWeightsOfCharZero instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Module.free_of_finite_type_torsion_free' IsSl2Triple.lie_e_f sl2 cartan_eq_lieSpan LieSubalgebra.subset_lieSpan Set.mem_range_self IsScalarTower.left smulCommClass_self LieModule.mem_genWeightSpace pow_one baseSupp_apply_smul_e sub_self neg_smul sub_neg_eq_add baseSupp_apply_smul_f lie_skew LieAlgebra.mem_corootSpace Submodule.subset_span IsAddTorsionFree.of_isTorsionFree IsDomain.toIsCancelMulZero LieAlgebra.IsKilling.eq_coroot_of_mem_corootSpace_of_two Nat.instAtLeastTwoHAddOfNat baseSupp_apply_h' A_diag_eq_two Int.cast_ofNat
ext 📖	—	A h e f cartan	—	—	—
ext_iff 📖	mathematical	—	A h e f cartan	—	ext
iSupIndep_rootSpace 📖	mathematical	—	iSupIndep LieSubmodule LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubmodule.instCompleteLattice Matrix.vecCons LieAlgebra.rootSpace LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing iSup LieSubmodule.instSupSet Nat.instMulZeroClass Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ AddMonoid.toNSMul Pi.addMonoid AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Pi.instNeg LinearMap.instNeg LieRing.ofAssociativeRing baseSupp Matrix.vecEmpty	—	LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan IsScalarTower.left LieSubalgebra.lieModule lieAlgebraSelfModule iSup_congr_Prop iSup_iSup_eq_left LinearMap.coe_sum Finset.sum_congr iSup_exists iSup_and iSup_comm nsmul_eq_mul AddMonoid.nat_smulCommClass' smul_neg Finset.sum_neg_distrib Algebra.to_smulCommClass Fintype.linearIndependent_iff linearIndependent_baseSupp Nat.cast_smul_eq_nsmul LinearMap.coe_zero_iff neg_eq_zero Set.disjoint_iff_forall_ne eq_neg_iff_add_eq_zero Pi.add_apply Nat.cast_eq_zero LieModule.iSupIndep_genWeightSpace iSup_union iSupIndep.disjoint_biSup_biSup LieSubmodule.instIsCompactlyGenerated LieSubmodule.instIsModularLattice Disjoint.union_right Disjoint.symm Disjoint.union_left
iSup_cartan_borelLower_borelUpper_eq_top 📖	mathematical	—	iSup LieSubmodule LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan LieSubalgebra.lieRing LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubmodule.instSupSet Matrix.vecCons LieSubalgebra.toLieSubmodule borelLower borelUpper Matrix.vecEmpty Top.top LieSubmodule.instTop	—	eq_top_iff span_ef LieSubalgebra.lieSpan_induction Set.mem_union LieSubmodule.mem_sup_right LieSubalgebra.subset_lieSpan LieSubmodule.mem_sup_left AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SMulMemClass.smul_mem LieSubmodule.instSMulMemClass lie_add add_lie LieSubalgebra.lie_mem lie_skew neg_mem_iff AddSubgroupClass.toNegMemClass LieSubmodule.lie_mem iSup_fin_three
instIsCartanSubalgebraCartanOfIsNoetherian 📖	mathematical	—	LieSubalgebra.IsCartanSubalgebra cartan	—	LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan LieAlgebra.eq_rootSpace_zero_iff_isCartan cartan_eq
instIsLieAbelianSubtypeMemLieSubalgebraCartan 📖	mathematical	—	IsLieAbelian LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan LieRingModule.toBracket LieSubalgebra.lieRing LieRing.toAddCommGroup lieRingSelfModule ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass	—	AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass cartan_eq_lieSpan LieSubalgebra.isLieAbelian_lieSpan_iff lie_h_h
lie_e_f_ne 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule e f NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
lie_h_e 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule h e SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup A	—	—
lie_h_f 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule h f SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup A	—	—
lie_h_h 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule h NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
linInd 📖	mathematical	—	LinearIndependent h CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule	—	—
linearIndepOn_root_baseSupp 📖	mathematical	—	LinearIndepOn LieModule.Weight LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike cartan Finite.of_fintype LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieRing.toAddCommGroup LieAlgebra.toModule LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain Field.toSemifield instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid isNoetherian_of_isNoetherianRing_of_finite DivisionRing.toRing Field.toDivisionRing IsSimpleModule.instIsNoetherian LieRing.ofAssociativeRing Semiring.toModule Ring.toSemiring instIsSimpleModule Finset Finset.instSetLike LieSubalgebra.root Module.Dual DivisionSemiring.toSemiring LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root LinearMap.addCommGroup RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass LieAlgebra.IsKilling.rootSystem LinearMap.addCommMonoid Set.range baseSupp'	—	Finite.of_fintype LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LinearIndependent.injective IsScalarTower.left Algebra.to_smulCommClass IsLocalRing.toNontrivial Field.instIsLocalRing linearIndependent_baseSupp LinearIndepOn.eq_1 linearIndependent_equiv
linearIndependent_baseSupp 📖	mathematical	—	LinearIndependent Module.Dual LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction baseSupp LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass	—	Finite.of_fintype Matrix.nondegenerate_iff_det_ne_zero RingHom.map_det eq_intCast RingHom.instRingHomClass Matrix.Nondegenerate.det_ne_zero Int.instIsDomain nondegen IsScalarTower.left linInd RingHomInvPair.ids coe_cartan_eq_span Algebra.to_smulCommClass Module.Basis.linearIndependent_coord Finset.sum_congr Int.cast_smul_eq_zsmul LinearIndependent.sum_smul_of_nondegenerate
nondegen 📖	mathematical	—	Matrix.Nondegenerate Int.instCommRing A	—	—
root_mem_or_mem_neg 📖	mathematical	—	Module.Dual LieSubalgebra EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubalgebra.instSetLike cartan Finite.of_fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.addCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring AddSubmonoid.instSetLike AddSubmonoid.closure Set.image LieModule.Weight LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule lieRingSelfModule LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors CommRing.toCommSemiring GroupWithZero.toNoZeroSMulDivisors DivisionSemiring.toGroupWithZero SubNegZeroMonoid.toSubNegMonoid SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian Ring.toSemiring instIsSimpleModule Finset Finset.instSetLike LieSubalgebra.root DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LieAlgebra.ofAssociativeAlgebra Algebra.to_smulCommClass LieAlgebra.IsKilling.rootSystem Set.range baseSupp' LinearMap.instNeg	—	Finite.of_fintype LieSubalgebra.lieModule lieAlgebraSelfModule LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra instIsCartanSubalgebraCartanOfIsNoetherian instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule IsScalarTower.left Algebra.to_smulCommClass Submodule.sum_smul_mem Submodule.subset_span LieModule.instLinearWeightsOfCharZero instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule Module.free_of_finite_type_torsion_free' Set.image_congr iSup_cartan_borelLower_borelUpper_eq_top iSup_union iSup_congr_Prop iSup_iSup_eq_left LieAlgebra.rootSpace_zero_eq LinearMap.coe_sum Finset.sum_congr nsmul_eq_mul iSup_exists iSup_and iSup_comm LieModule.trivialIsNilpotent instIsLieAbelianSubtypeMemLieSubalgebraCartan LieAlgebra.rootSpace.congr_simp smul_neg Finset.sum_neg_distrib iSup_fin_three cartan_eq borelUpper_eq borelLower_eq iSupIndep.mem_of_biSup_eq_top LieModule.iSupIndep_genWeightSpace LieModule.Weight.genWeightSpace_ne_bot LinearMap.coe_injective neg_neg
sl2 📖	mathematical	—	IsSl2Triple h e f	—	—
span_ef 📖	mathematical	—	LieSubalgebra.lieSpan Set Set.instUnion Set.range e f Top.top LieSubalgebra LieSubalgebra.instTop	—	—
symm_A 📖	mathematical	—	A symm	—	—
symm_baseSupp 📖	mathematical	—	baseSupp symm Pi.instNeg Module.Dual LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instNeg LieRing.ofAssociativeRing CommRing.toRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring	—	IsScalarTower.left linInd RingHomInvPair.ids coe_cartan_eq_span LinearIndependent.neg RingHomCompTriple.ids Submodule.span_neg Module.Basis.span_neg LinearMap.ext map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass neg_neg AddGroup.int_smulCommClass' Finset.sum_congr smul_neg Finset.sum_neg_distrib
symm_cartan 📖	mathematical	—	cartan symm	—	—
symm_e 📖	mathematical	—	e symm f	—	—
symm_f 📖	mathematical	—	f symm e	—	—
symm_h 📖	mathematical	—	h symm Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	—
symm_h' 📖	mathematical	—	h' symm LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike cartan NegMemClass.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup AddSubgroupClass.toNegMemClass AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieSubalgebra.instAddSubgroupClass	—	—
symm_symm 📖	mathematical	—	symm	—	ext Matrix.ext neg_neg LieSubalgebra.ext

---

← Back to Index