Subalgebra

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

Statistics

Metric	Count
Definitions lieSubalgebraMap, ofEq, ofInjective, ofSubalgebras, equivRangeOfInjective, range, rangeRestrict, restrictLie, LieSubalgebra, addCommMonoid, comap, completeLattice, equivOfLe, gi, incl, incl', inclusion, instAdd, instBot, instBracketSubtypeMem, instInfSet, instMin, instModuleSubtypeMemOfIsScalarTower, instPartialOrder, instPartialOrder_1, instSetLike, instTop, instZero, lieAlgebra, lieRing, lieRingModule, lieSpan, map, ofLe, toSubmodule, instCoeLieSubalgebraSubmodule, instInhabitedLieSubalgebra, instZeroLieSubalgebra	38
Theorems lieSubalgebraMap_apply, ofEq_apply, ofInjective_apply, ofSubalgebras_apply, ofSubalgebras_symm_apply, coe_range, equivRangeOfInjective_apply, mem_range, mem_range_self, rangeRestrict_apply, range_eq_map, surjective_rangeRestrict, coe_restrictLie, add_eq_sup, add_mem, bot_coe, bot_toSubmodule, coe_bracket, coe_bracket_of_module, coe_incl, coe_incl', coe_inclusion, coe_inf, coe_injective, coe_lieSpan_eq_span_of_forall_lie_eq_zero, coe_lieSpan_submodule_eq_iff, coe_ofLe, coe_sInf, coe_set_eq, coe_toSubmodule, coe_zero_iff_zero, comap_lieSpan_range_eq, disjoint_toSubmodule, eq_bot_iff, equivOfLe_apply, ext, ext_iff, ext_iff', gc_map_comap, incl_range, inclusion_apply, inclusion_injective, inf_toSubmodule, instAddSubgroupClass, instCanonicallyOrderedAdd, instIsArtinianSubtypeMem, instIsCentralScalarSubtypeMem, instIsLieTowerSubtypeMem, instIsNoetherianSubtypeMem, instIsOrderedAddMonoid, instIsScalarTowerSubtypeMem, instSMulMemClass, le_def, lieModule, lieSpan_eq, lieSpan_induction, lieSpan_le, lieSpan_lieSpan_coe_preimage, lieSpan_mono, lieSpan_neg, lie_mem, lie_mem', map_le_iff_le_comap, mem_bot, mem_carrier, mem_coe, mem_comap, mem_inf, mem_lieSpan, mem_map, mem_map_submodule, mem_mk_iff, mem_mk_iff', mem_ofLe, mem_toSubmodule, mem_top, mk_coe, ofLe_eq_comap_incl, sInf_glb, sInf_toSubmodule, smul_mem, span_empty, span_iUnion, span_union, span_univ, sub_mem, submodule_span_le_lieSpan, subset_lieSpan, subsingleton_bot, subsingleton_of_bot, toSubmodule_eq_bot, toSubmodule_eq_top, toSubmodule_inj, toSubmodule_injective, toSubmodule_le_toSubmodule, toSubmodule_mk, top_coe, top_toSubmodule, wellFoundedGT_of_noetherian, zero_mem, exists_lieSubalgebra_coe_eq_iff	101
Total	139

LieEquiv

Definitions

Name	Category	Theorems
lieSubalgebraMap 📖	CompOp	1 math math: lieSubalgebraMap_apply
ofEq 📖	CompOp	1 math math: ofEq_apply
ofInjective 📖	CompOp	1 math math: ofInjective_apply
ofSubalgebras 📖	CompOp	2 math math: ofSubalgebras_apply, ofSubalgebras_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieSubalgebraMap_apply 📖	mathematical	—	LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.map toLieHom DFunLike.coe LieEquiv LieSubalgebra.lieRing LieSubalgebra.lieAlgebra EquivLike.toFunLike instEquivLike lieSubalgebraMap	—	—
ofEq_apply 📖	mathematical	SetLike.coe LieSubalgebra LieSubalgebra.instSetLike	LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike DFunLike.coe LieEquiv LieSubalgebra.lieRing LieSubalgebra.lieAlgebra EquivLike.toFunLike instEquivLike ofEq	—	—
ofInjective_apply 📖	mathematical	DFunLike.coe LieHom LieHom.instFunLike	LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieHom.range DFunLike.coe LieEquiv LieSubalgebra.lieRing LieSubalgebra.lieAlgebra EquivLike.toFunLike instEquivLike ofInjective LieHom LieHom.instFunLike	—	—
ofSubalgebras_apply 📖	mathematical	LieSubalgebra.map toLieHom	LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike DFunLike.coe LieEquiv LieSubalgebra.lieRing LieSubalgebra.lieAlgebra EquivLike.toFunLike instEquivLike ofSubalgebras	—	—
ofSubalgebras_symm_apply 📖	mathematical	LieSubalgebra.map toLieHom	LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike DFunLike.coe LieEquiv LieSubalgebra.lieRing LieSubalgebra.lieAlgebra EquivLike.toFunLike instEquivLike symm ofSubalgebras	—	—

LieHom

Definitions

Name	Category	Theorems
equivRangeOfInjective 📖	CompOp	1 math math: equivRangeOfInjective_apply
range 📖	CompOp	37 math math: LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, ker_snd, LieDerivation.IsKilling.instIsKilling_range_ad, surjective_rangeRestrict, isIdealMorphism_def, quotKerEquivRange_toFun, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, equivRangeOfInjective_apply, mem_range_self, LieModule.isNilpotent_range_toEnd_iff, isNilpotent_range, LieSubalgebra.incl_range, IsIdealMorphism.eq, LieDerivation.IsKilling.killingForm_restrict_range_ad, LieIdeal.incl_range, LieDerivation.IsKilling.ad_mem_orthogonal_of_mem_orthogonal, rangeRestrict_apply, coe_range, range_eq_top, range_inr, range_eq_map, range_inl, quotKerEquivRange_invFun, idealRange_eq_lieSpan_range, LieDerivation.IsKilling.range_ad_eq_top, range_toSubmodule, isSolvable_range, ker_fst, range_subset_idealRange, LieEquiv.ofInjective_apply, LieAlgebra.IsExtension.exact, LieAlgebra.isNilpotent_range_ad_iff, LieAlgebra.IsExtension.range_eq_top, mem_range, LieModule.coe_lcs_range_toEnd_eq, LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, range_eq_ker_iff
rangeRestrict 📖	CompOp	2 math math: surjective_rangeRestrict, rangeRestrict_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_range 📖	mathematical	—	SetLike.coe LieSubalgebra LieSubalgebra.instSetLike range Set.range DFunLike.coe LieHom instFunLike	—	LinearMap.coe_range RingHomSurjective.ids
equivRangeOfInjective_apply 📖	mathematical	DFunLike.coe LieHom instFunLike	DFunLike.coe LieEquiv LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike range LieSubalgebra.lieRing LieSubalgebra.lieAlgebra EquivLike.toFunLike LieEquiv.instEquivLike equivRangeOfInjective LieHom instFunLike mem_range_self	—	—
mem_range 📖	mathematical	—	LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike range DFunLike.coe LieHom instFunLike	—	LinearMap.mem_range RingHomSurjective.ids
mem_range_self 📖	mathematical	—	LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike range DFunLike.coe LieHom instFunLike	—	LinearMap.mem_range_self RingHomSurjective.ids
rangeRestrict_apply 📖	mathematical	—	DFunLike.coe LieHom LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike range LieSubalgebra.lieRing LieSubalgebra.lieAlgebra instFunLike rangeRestrict mem_range_self	—	—
range_eq_map 📖	mathematical	—	range LieSubalgebra.map Top.top LieSubalgebra LieSubalgebra.instTop	—	LieSubalgebra.ext
surjective_rangeRestrict 📖	mathematical	—	LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike range DFunLike.coe LieHom LieSubalgebra.lieRing LieSubalgebra.lieAlgebra instFunLike rangeRestrict	—	mem_range mem_range_self

LieModuleHom

Definitions

Name	Category	Theorems
restrictLie 📖	CompOp	2 math math: coe_restrictLie, LieSubmodule.map_restrictLie_incl_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_restrictLie 📖	mathematical	—	DFunLike.coe LieModuleHom LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieRingModule instFunLike restrictLie	—	—

LieSubalgebra

Definitions

Name	Category	Theorems
addCommMonoid 📖	CompOp	1 math math: instIsOrderedAddMonoid
comap 📖	CompOp	5 math math: map_le_iff_le_comap, mem_comap, ofLe_eq_comap_incl, gc_map_comap, comap_lieSpan_range_eq
completeLattice 📖	CompOp	4 math math: span_union, disjoint_toSubmodule, span_iUnion, add_eq_sup
equivOfLe 📖	CompOp	1 math math: equivOfLe_apply
gi 📖	CompOp	—
incl 📖	CompOp	6 math math: incl_range, LieModule.coe_genWeightSpace_of_top, coe_incl, ofLe_eq_comap_incl, comap_lieSpan_range_eq, ad_comp_incl_eq
incl' 📖	CompOp	2 math math: coe_incl', LieAlgebra.rootSpace_comap_eq_genWeightSpace
inclusion 📖	CompOp	4 math math: inclusion_apply, equivOfLe_apply, coe_inclusion, inclusion_injective
instAdd 📖	CompOp	2 math math: instCanonicallyOrderedAdd, add_eq_sup
instBot 📖	CompOp	8 math math: subsingleton_bot, bot_coe, mem_bot, subsingleton_of_bot, span_empty, toSubmodule_eq_bot, bot_toSubmodule, eq_bot_iff
instBracketSubtypeMem 📖	CompOp	7 math math: LieAlgebra.IsKilling.chainLength_nsmul, coe_bracket_of_module, LieAlgebra.Basis.baseSupp_apply_smul_f, instIsLieTowerSubtypeMem, LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace, LieAlgebra.Basis.baseSupp_apply_smul_e, LieAlgebra.IsKilling.chainLength_smul
instInfSet 📖	CompOp	3 math math: sInf_toSubmodule, coe_sInf, sInf_glb
instMin 📖	CompOp	3 math math: mem_inf, coe_inf, inf_toSubmodule
instModuleSubtypeMemOfIsScalarTower 📖	CompOp	55 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieAlgebra.finrank_engel, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieIdeal.reflectionPerm_mem_rootSet_iff, LieAlgebra.Basis.borelLower_le_biSup, LieIdeal.toInvtRootSubmodule_mono, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, LieAlgebra.Basis.borelUpper_eq, LieAlgebra.Basis.linearIndepOn_root_baseSupp, LieIdeal.rootSpan_mem_invtRootSubmodule, LieAlgebra.Basis.coroot_eq_h', LieAlgebra.Basis.symm_baseSupp, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', LieAlgebra.Basis.baseSupp_apply_smul_f, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, RootPairing.GeckConstruction.span_range_h'_eq_top, LieAlgebra.Basis.iSupIndep_rootSpace, coe_incl', LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.isSimple_iff_isIrreducible, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, LieAlgebra.Basis.baseSupp_apply_smul_e, LieAlgebra.rootSpace_comap_eq_genWeightSpace, LieAlgebra.SpecialLinear.val_single, instIsNoetherianSubtypeMem, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, LieAlgebra.Basis.cartanMatrix_base_eq, LieAlgebra.rank_le_finrank_engel, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieAlgebra.Basis.borelUpper_le_biSup, LieAlgebra.mem_corootSpace', LieAlgebra.IsKilling.lieIdealOrderIso_right_inv, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.Basis.borelLower_eq, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, LieAlgebra.Basis.root_mem_or_mem_neg, LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.isRegular_iff_finrank_engel_eq_rank, instIsScalarTowerSubtypeMem, LieAlgebra.SpecialLinear.val_singleSubSingle, LieAlgebra.Basis.coe_baseSupportEquiv_apply, LieAlgebra.Basis.linearIndependent_baseSupp, instIsCentralScalarSubtypeMem, LieAlgebra.Basis.baseSupp_apply_h', LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.IsKilling.rootSystem_root_apply, instIsArtinianSubtypeMem, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple
instPartialOrder 📖	CompOp	—
instPartialOrder_1 📖	CompOp	16 math math: le_normalizer, toSubmodule_le_toSubmodule, lieSpan_mono, LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer, map_le_iff_le_comap, instCanonicallyOrderedAdd, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, disjoint_toSubmodule, lieSpan_le, instIsOrderedAddMonoid, wellFoundedGT_of_noetherian, le_def, sInf_glb, LieAlgebra.le_zeroRootSubalgebra, gc_map_comap, LieAlgebra.engel_isBot_of_isMin
instSetLike 📖	CompOp	303 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieModule.Weight.IsZero.neg, LieDerivation.IsKilling.instIsKilling_range_ad, inclusion_apply, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, isLieAbelian_lieSpan_iff, skewAdjointMatricesLieSubalgebraEquivTranspose_apply, RootPairing.GeckConstruction.instHasTrivialRadical, LieAlgebra.Orthogonal.mem_so, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, LieHom.surjective_rangeRestrict, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, LieAlgebra.finrank_engel, skewAdjointLieSubalgebraEquiv_apply, mem_map_submodule, equivOfLe_apply, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, LieIdeal.reflectionPerm_mem_rootSet_iff, LieAlgebra.Basis.borelLower_le_biSup, LieModule.Weight.IsNonZero.neg, toEnd_eq, LieAlgebra.coe_zeroRootSubalgebra, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, subsingleton_bot, LieModule.isNilpotent_of_top_iff, bot_coe, LieAlgebra.Basis.symm_h', mem_ofLe, skewAdjointLieSubalgebraEquiv_symm_apply, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, mem_bot, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieAlgebra.IsKilling.reflectRoot_isNonZero, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieAlgebra.IsKilling.chainLength_nsmul, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieIdeal.toInvtRootSubmodule_mono, LieHom.equivRangeOfInjective_apply, LieHom.mem_range_self, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right, LieModule.isNilpotent_range_toEnd_iff, LieAlgebra.Basis.cartan_eq, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieIdeal.coe_toLieSubalgebra, LieHom.isNilpotent_range, IsCartanSubalgebra.nilpotent, mem_toSubmodule, mem_carrier, LieAlgebra.Basis.borelUpper_eq, LieAlgebra.Basis.linearIndepOn_root_baseSupp, engel_carrier, coe_injective, LieIdeal.rootSpan_mem_invtRootSubmodule, LieAlgebra.Basis.coroot_eq_h', isNonZero_coe_root, LieModule.traceForm_lieSubalgebra_mk_right, LieAlgebra.IsKilling.chainLength_zero, incl_range, ideal_in_normalizer, toEnd_mk, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.Basis.symm_baseSupp, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', IsSl2Triple.mem_toLieSubalgebra_iff, LieAlgebra.mem_biSup_genWeightSpace_of, exists_nested_lieIdeal_coe_eq_iff, LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop, coe_bracket_of_module, LieAlgebra.Basis.baseSupp_apply_smul_f, coe_normalizer_eq_normalizer, LieModule.exists_forall_mem_corootSpace_smul_add_eq_zero, coe_toSubmodule, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, coe_ad_pow, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, subsingleton_of_bot, add_mem, mem_toLieSubmodule, self_mem_engel, LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieDerivation.IsKilling.killingForm_restrict_range_ad, coe_inclusion, Derivation.Compatible.mem, LieEquiv.ofEq_apply, LieAlgebra.IsKilling.chainLength_neg, LieSubmodule.mem_restr, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, RootPairing.GeckConstruction.span_range_h'_eq_top, LieAlgebra.Basis.instIsLieAbelianSubtypeMemLieSubalgebraCartan, coe_sInf, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieEquiv.ofSubalgebras_apply, coe_set_eq, LieModuleHom.coe_restrictLie, LieAlgebra.Basis.iSupIndep_rootSpace, LieAlgebra.IsKilling.apply_coroot_eq_cast, coe_incl', RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', RootPairing.GeckConstruction.basis_A_eq, IsSl2Triple.h_eq_coroot, LieIdeal.restr_eq_iSup_sl2SubmoduleOfRoot, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.isSimple_iff_isIrreducible, LieHom.rangeRestrict_apply, LieAlgebra.SpecialLinear.sl_bracket, LieAlgebra.lieIdeal_eq_iSup_inf_genWeightSpace, subset_lieSpan, LieHom.coe_range, LieModule.Weight.isZero_neg, instIsNilpotentSubtypeMemLieSubalgebraTop, mem_comap, LieSubmodule.map_restrictLie_incl_top, mem_inf, LieEquiv.lieSubalgebraMap_apply, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieAlgebra.IsKilling.rootSpace_one_div_two_smul, LieAlgebra.rootSpace_zero_eq, LieDerivation.eqOn_lieSpan, mem_skewAdjointMatricesLieSubalgebra, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, lieModule, LieIdeal.mem_rootSet_of_mem_rootSpan, LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet, RootPairing.GeckConstruction.instIsIrreducible, mem_engel_iff, ucs_eq_self_of_isCartanSubalgebra, LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule, Derivation.Compatible.apply, isNilpotent_of_forall_le_engel, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, instIsLieTowerSubtypeMem, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, coe_bracket, isNilpotent_ad_of_isNilpotent_ad, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieAlgebra.toEnd_pow_apply_mem, LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace, LieModule.coe_genWeightSpace_of_top, LieIdeal.mem_rootSet, LieAlgebra.Basis.baseSupp_apply_smul_e, LieHom.quotKerEquivRange_invFun, top_coe, coe_ofLe, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, inclusion_injective, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, isCartanSubalgebra_iff_isUcsLimit, RootPairing.GeckConstruction.h_mem_cartanSubalgebra', LieAlgebra.rootSpace_comap_eq_genWeightSpace, LieModule.traceForm_lieSubalgebra_mk_left, LieIdeal.rootSpace_le_of_apply_coroot_ne_zero, ext_iff', LieAlgebra.restrict_killingForm, mem_skewAdjointMatricesLieSubalgebra_unit_smul, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, coe_toLieSubmodule, instIsNilpotentSubtypeMemOfIsCartanSubalgebra, LieAlgebra.IsKilling.root_apply_coroot, LieAlgebra.IsKilling.coroot_neg, mem_normalizer_iff', LieHom.idealRange_eq_lieSpan_range, coe_inf, LieAlgebra.SpecialLinear.val_single, LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_corootSpace, instIsNoetherianSubtypeMem, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, LieIdeal.mem_toLieSubalgebra, LieAlgebra.Basis.cartanMatrix_base_eq, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, RootPairing.GeckConstruction.h_mem_lieAlgebra, exists_lieIdeal_coe_eq_iff, LieAlgebra.rank_le_finrank_engel, topEquiv_apply, instNontrivialSubtypeMemOfIsCartanSubalgebra, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul, LieAlgebra.lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace, LieHom.isSolvable_range, normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.chainTopCoeff_zero_right, coe_incl, ext_iff, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, lieSpan_le, mk_coe, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, LieHom.range_subset_idealRange, LieEquiv.ofSubalgebras_symm_apply, coe_zero_iff_zero, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, RootPairing.GeckConstruction.ωConj_mem_of_mem, LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainLength_zero_right, LieAlgebra.IsKilling.chainLength_smul, LieEquiv.ofInjective_apply, sub_mem, LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace, LieAlgebra.Basis.borelUpper_le_biSup, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.mem_corootSpace', mem_map, LieAlgebra.IsKilling.lieIdealOrderIso_right_inv, zero_mem, LieAlgebra.eq_rootSpace_zero_iff_isCartan, LieAlgebra.isNilpotent_range_ad_iff, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.Basis.borelLower_eq, mem_mk_iff', LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieAlgebra.IsKilling.chainBotCoeff_zero_right, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, exists_nested_lieIdeal_ofLe_normalizer, LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot, LieAlgebra.Basis.root_mem_or_mem_neg, LieHom.mem_range, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.rootSpace_two_smul, LieAlgebra.isRegular_iff_finrank_engel_eq_rank, instIsScalarTowerSubtypeMem, mem_coe, LieAlgebra.mem_corootSpace, RootPairing.GeckConstruction.f_mem_lieAlgebra, LieIdeal.corootSubmodule_le, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, RootPairing.GeckConstruction.e_mem_lieAlgebra, LieAlgebra.SpecialLinear.val_singleSubSingle, lieSpan_eq, LieAlgebra.IsKilling.span_weight_eq_top, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left, skewAdjointMatricesLieSubalgebraEquiv_apply, le_def, LieAlgebra.Basis.coe_linearMap_baseSupp', LieAlgebra.isNilpotent_ad_of_isNilpotent, LieModule.Weight.toLinear_neg, Derivation.Compatible.mk_left, LieSubmodule.restr_toSubmodule, LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, mem_lieSpan, mem_top, ofLe_eq_comap_incl, instSMulMemClass, LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.Basis.coe_baseSupportEquiv_apply, LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff, LieAlgebra.Basis.linearIndependent_baseSupp, instIsCentralScalarSubtypeMem, lieSpan_lieSpan_coe_preimage, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieAlgebra.rootSpaceProduct_tmul, mem_normalizer_iff, LieIdeal.root_apply_eq_zero_of_notMem_rootSet, LieAlgebra.Basis.baseSupp_apply_h', LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.IsKilling.rootSystem_root_apply, LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule, LieAlgebra.IsKilling.lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, instIsArtinianSubtypeMem, Derivation.Compatible.mk_right, normalizer_eq_self_of_isCartanSubalgebra, smul_mem, LieModule.Weight.coe_neg, mem_mk_iff, instAddSubgroupClass, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, coe_ad, lie_mem, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, comap_lieSpan_range_eq, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra, LieAlgebra.engel_isBot_of_isMin, ad_comp_incl_eq
instTop 📖	CompOp	22 math math: top_toSubmodule, span_univ, LieModule.isNilpotent_of_top_iff, LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop, instIsNilpotentSubtypeMemLieSubalgebraTop, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieHom.range_eq_top, LieHom.range_eq_map, LieModule.coe_genWeightSpace_of_top, top_coe, LieAlgebra.Basis.span_ef, engel_zero, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, topEquiv_apply, LieDerivation.IsKilling.range_ad_eq_top, toSubmodule_eq_top, LieIdeal.normalizer_eq_top, LieAlgebra.top_isCartanSubalgebra_of_nilpotent, LieIdeal.top_toLieSubalgebra, LieAlgebra.IsExtension.range_eq_top, mem_top, lieSpan_lieSpan_coe_preimage
instZero 📖	CompOp	—
lieAlgebra 📖	CompOp	169 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieModule.Weight.IsZero.neg, LieDerivation.IsKilling.instIsKilling_range_ad, inclusion_apply, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, skewAdjointMatricesLieSubalgebraEquivTranspose_apply, RootPairing.GeckConstruction.instHasTrivialRadical, LieHom.surjective_rangeRestrict, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, skewAdjointLieSubalgebraEquiv_apply, equivOfLe_apply, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, LieIdeal.reflectionPerm_mem_rootSet_iff, LieModule.Weight.IsNonZero.neg, toEnd_eq, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, mem_ofLe, skewAdjointLieSubalgebraEquiv_symm_apply, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieAlgebra.IsKilling.reflectRoot_isNonZero, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieIdeal.toInvtRootSubmodule_mono, LieHom.equivRangeOfInjective_apply, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieAlgebra.Basis.linearIndepOn_root_baseSupp, LieIdeal.rootSpan_mem_invtRootSubmodule, LieAlgebra.Basis.coroot_eq_h', isNonZero_coe_root, LieModule.traceForm_lieSubalgebra_mk_right, LieAlgebra.IsKilling.chainLength_zero, incl_range, toEnd_mk, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', LieAlgebra.mem_biSup_genWeightSpace_of, exists_nested_lieIdeal_coe_eq_iff, coe_normalizer_eq_normalizer, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, coe_ad_pow, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, subsingleton_of_bot, LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieDerivation.IsKilling.killingForm_restrict_range_ad, coe_inclusion, LieEquiv.ofEq_apply, LieAlgebra.IsKilling.chainLength_neg, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, RootPairing.GeckConstruction.span_range_h'_eq_top, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieEquiv.ofSubalgebras_apply, LieAlgebra.IsKilling.apply_coroot_eq_cast, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', RootPairing.GeckConstruction.basis_A_eq, LieIdeal.restr_eq_iSup_sl2SubmoduleOfRoot, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.isSimple_iff_isIrreducible, LieHom.rangeRestrict_apply, LieAlgebra.lieIdeal_eq_iSup_inf_genWeightSpace, LieModule.Weight.isZero_neg, LieEquiv.lieSubalgebraMap_apply, LieAlgebra.IsKilling.rootSpace_one_div_two_smul, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, lieModule, LieIdeal.mem_rootSet_of_mem_rootSpan, LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet, ucs_eq_self_of_isCartanSubalgebra, LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, isNilpotent_ad_of_isNilpotent_ad, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieAlgebra.toEnd_pow_apply_mem, LieModule.coe_genWeightSpace_of_top, LieIdeal.mem_rootSet, LieHom.quotKerEquivRange_invFun, coe_ofLe, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, inclusion_injective, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, isCartanSubalgebra_iff_isUcsLimit, RootPairing.GeckConstruction.h_mem_cartanSubalgebra', LieAlgebra.rootSpace_comap_eq_genWeightSpace, LieModule.traceForm_lieSubalgebra_mk_left, LieAlgebra.restrict_killingForm, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, LieAlgebra.IsKilling.root_apply_coroot, LieAlgebra.IsKilling.coroot_neg, LieAlgebra.Basis.cartanMatrix_base_eq, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, topEquiv_apply, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul, LieAlgebra.lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace, normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.chainTopCoeff_zero_right, coe_incl, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, LieEquiv.ofSubalgebras_symm_apply, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainLength_zero_right, LieEquiv.ofInjective_apply, LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.mem_corootSpace', LieAlgebra.IsKilling.lieIdealOrderIso_right_inv, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.IsKilling.coroot_zero, LieAlgebra.IsKilling.chainBotCoeff_zero_right, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, exists_nested_lieIdeal_ofLe_normalizer, LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot, LieAlgebra.Basis.root_mem_or_mem_neg, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.rootSpace_two_smul, LieAlgebra.mem_corootSpace, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieAlgebra.IsKilling.span_weight_eq_top, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left, skewAdjointMatricesLieSubalgebraEquiv_apply, LieAlgebra.Basis.coe_linearMap_baseSupp', LieAlgebra.isNilpotent_ad_of_isNilpotent, LieModule.Weight.toLinear_neg, LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, ofLe_eq_comap_incl, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.Basis.coe_baseSupportEquiv_apply, lieSpan_lieSpan_coe_preimage, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieAlgebra.rootSpaceProduct_tmul, LieIdeal.root_apply_eq_zero_of_notMem_rootSet, LieAlgebra.IsKilling.rootSystem_root_apply, LieAlgebra.IsKilling.lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, normalizer_eq_self_of_isCartanSubalgebra, LieModule.Weight.coe_neg, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, coe_ad, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, comap_lieSpan_range_eq, ad_comp_incl_eq
lieRing 📖	CompOp	226 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieModule.Weight.IsZero.neg, LieDerivation.IsKilling.instIsKilling_range_ad, inclusion_apply, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, isLieAbelian_lieSpan_iff, skewAdjointMatricesLieSubalgebraEquivTranspose_apply, RootPairing.GeckConstruction.instHasTrivialRadical, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, LieHom.surjective_rangeRestrict, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, LieAlgebra.finrank_engel, skewAdjointLieSubalgebraEquiv_apply, equivOfLe_apply, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, LieIdeal.reflectionPerm_mem_rootSet_iff, LieAlgebra.Basis.borelLower_le_biSup, LieModule.Weight.IsNonZero.neg, toEnd_eq, LieAlgebra.coe_zeroRootSubalgebra, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, LieModule.isNilpotent_of_top_iff, mem_ofLe, skewAdjointLieSubalgebraEquiv_symm_apply, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieAlgebra.IsKilling.reflectRoot_isNonZero, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieIdeal.toInvtRootSubmodule_mono, LieHom.equivRangeOfInjective_apply, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right, LieModule.isNilpotent_range_toEnd_iff, LieAlgebra.Basis.cartan_eq, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieHom.isNilpotent_range, IsCartanSubalgebra.nilpotent, LieAlgebra.Basis.borelUpper_eq, LieAlgebra.Basis.linearIndepOn_root_baseSupp, LieIdeal.rootSpan_mem_invtRootSubmodule, LieAlgebra.Basis.coroot_eq_h', isNonZero_coe_root, LieModule.traceForm_lieSubalgebra_mk_right, LieAlgebra.IsKilling.chainLength_zero, incl_range, toEnd_mk, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.Basis.symm_baseSupp, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', LieAlgebra.mem_biSup_genWeightSpace_of, exists_nested_lieIdeal_coe_eq_iff, LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop, LieAlgebra.Basis.baseSupp_apply_smul_f, coe_normalizer_eq_normalizer, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, coe_ad_pow, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, subsingleton_of_bot, mem_toLieSubmodule, LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieDerivation.IsKilling.killingForm_restrict_range_ad, coe_inclusion, LieEquiv.ofEq_apply, LieAlgebra.IsKilling.chainLength_neg, LieSubmodule.mem_restr, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, RootPairing.GeckConstruction.span_range_h'_eq_top, LieAlgebra.Basis.instIsLieAbelianSubtypeMemLieSubalgebraCartan, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieEquiv.ofSubalgebras_apply, LieModuleHom.coe_restrictLie, LieAlgebra.Basis.iSupIndep_rootSpace, LieAlgebra.IsKilling.apply_coroot_eq_cast, coe_incl', RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', RootPairing.GeckConstruction.basis_A_eq, LieIdeal.restr_eq_iSup_sl2SubmoduleOfRoot, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.isSimple_iff_isIrreducible, LieHom.rangeRestrict_apply, LieAlgebra.SpecialLinear.sl_bracket, LieAlgebra.lieIdeal_eq_iSup_inf_genWeightSpace, LieModule.Weight.isZero_neg, instIsNilpotentSubtypeMemLieSubalgebraTop, LieSubmodule.map_restrictLie_incl_top, LieEquiv.lieSubalgebraMap_apply, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieAlgebra.IsKilling.rootSpace_one_div_two_smul, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, lieModule, LieIdeal.mem_rootSet_of_mem_rootSpan, LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet, RootPairing.GeckConstruction.instIsIrreducible, ucs_eq_self_of_isCartanSubalgebra, LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule, isNilpotent_of_forall_le_engel, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, coe_bracket, isNilpotent_ad_of_isNilpotent_ad, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieAlgebra.toEnd_pow_apply_mem, LieModule.coe_genWeightSpace_of_top, LieIdeal.mem_rootSet, LieAlgebra.Basis.baseSupp_apply_smul_e, LieHom.quotKerEquivRange_invFun, coe_ofLe, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, inclusion_injective, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, isCartanSubalgebra_iff_isUcsLimit, RootPairing.GeckConstruction.h_mem_cartanSubalgebra', LieAlgebra.rootSpace_comap_eq_genWeightSpace, LieModule.traceForm_lieSubalgebra_mk_left, LieIdeal.rootSpace_le_of_apply_coroot_ne_zero, LieAlgebra.restrict_killingForm, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, coe_toLieSubmodule, instIsNilpotentSubtypeMemOfIsCartanSubalgebra, LieAlgebra.IsKilling.root_apply_coroot, LieAlgebra.IsKilling.coroot_neg, LieAlgebra.SpecialLinear.val_single, instIsNoetherianSubtypeMem, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, LieAlgebra.Basis.cartanMatrix_base_eq, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, LieAlgebra.rank_le_finrank_engel, topEquiv_apply, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul, LieAlgebra.lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace, LieHom.isSolvable_range, normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.chainTopCoeff_zero_right, coe_incl, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, LieEquiv.ofSubalgebras_symm_apply, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainLength_zero_right, LieEquiv.ofInjective_apply, LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace, LieAlgebra.Basis.borelUpper_le_biSup, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.mem_corootSpace', LieAlgebra.IsKilling.lieIdealOrderIso_right_inv, LieAlgebra.isNilpotent_range_ad_iff, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.Basis.borelLower_eq, LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieAlgebra.IsKilling.chainBotCoeff_zero_right, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, exists_nested_lieIdeal_ofLe_normalizer, LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot, LieAlgebra.Basis.root_mem_or_mem_neg, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.rootSpace_two_smul, LieAlgebra.isRegular_iff_finrank_engel_eq_rank, instIsScalarTowerSubtypeMem, LieAlgebra.mem_corootSpace, LieIdeal.corootSubmodule_le, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieAlgebra.SpecialLinear.val_singleSubSingle, LieAlgebra.IsKilling.span_weight_eq_top, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left, skewAdjointMatricesLieSubalgebraEquiv_apply, LieAlgebra.Basis.coe_linearMap_baseSupp', LieAlgebra.isNilpotent_ad_of_isNilpotent, LieModule.Weight.toLinear_neg, LieSubmodule.restr_toSubmodule, LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, ofLe_eq_comap_incl, LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.Basis.coe_baseSupportEquiv_apply, LieAlgebra.Basis.linearIndependent_baseSupp, instIsCentralScalarSubtypeMem, lieSpan_lieSpan_coe_preimage, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieAlgebra.rootSpaceProduct_tmul, LieIdeal.root_apply_eq_zero_of_notMem_rootSet, LieAlgebra.Basis.baseSupp_apply_h', LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.IsKilling.rootSystem_root_apply, LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule, LieAlgebra.IsKilling.lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, instIsArtinianSubtypeMem, normalizer_eq_self_of_isCartanSubalgebra, LieModule.Weight.coe_neg, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, coe_ad, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, comap_lieSpan_range_eq, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra, ad_comp_incl_eq
lieRingModule 📖	CompOp	147 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, LieModule.Weight.IsZero.neg, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, LieIdeal.reflectionPerm_mem_rootSet_iff, LieAlgebra.Basis.borelLower_le_biSup, LieModule.Weight.IsNonZero.neg, toEnd_eq, LieAlgebra.coe_zeroRootSubalgebra, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, LieModule.isNilpotent_of_top_iff, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieAlgebra.IsKilling.reflectRoot_isNonZero, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieIdeal.toInvtRootSubmodule_mono, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right, LieModule.isNilpotent_range_toEnd_iff, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieAlgebra.Basis.borelUpper_eq, LieAlgebra.Basis.linearIndepOn_root_baseSupp, LieIdeal.rootSpan_mem_invtRootSubmodule, LieAlgebra.Basis.coroot_eq_h', isNonZero_coe_root, LieModule.traceForm_lieSubalgebra_mk_right, LieAlgebra.IsKilling.chainLength_zero, toEnd_mk, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', LieAlgebra.mem_biSup_genWeightSpace_of, coe_normalizer_eq_normalizer, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, mem_toLieSubmodule, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieAlgebra.IsKilling.chainLength_neg, LieSubmodule.mem_restr, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieModuleHom.coe_restrictLie, LieAlgebra.Basis.iSupIndep_rootSpace, LieAlgebra.IsKilling.apply_coroot_eq_cast, coe_incl', LieIdeal.restr_eq_iSup_sl2SubmoduleOfRoot, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.isSimple_iff_isIrreducible, LieAlgebra.lieIdeal_eq_iSup_inf_genWeightSpace, LieModule.Weight.isZero_neg, LieSubmodule.map_restrictLie_incl_top, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieAlgebra.IsKilling.rootSpace_one_div_two_smul, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, lieModule, LieIdeal.mem_rootSet_of_mem_rootSpan, LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet, RootPairing.GeckConstruction.instIsIrreducible, ucs_eq_self_of_isCartanSubalgebra, LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieAlgebra.toEnd_pow_apply_mem, LieModule.coe_genWeightSpace_of_top, LieIdeal.mem_rootSet, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, isCartanSubalgebra_iff_isUcsLimit, LieAlgebra.rootSpace_comap_eq_genWeightSpace, LieModule.traceForm_lieSubalgebra_mk_left, LieIdeal.rootSpace_le_of_apply_coroot_ne_zero, LieAlgebra.restrict_killingForm, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, coe_toLieSubmodule, LieAlgebra.IsKilling.root_apply_coroot, LieAlgebra.IsKilling.coroot_neg, LieAlgebra.Basis.cartanMatrix_base_eq, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul, LieAlgebra.lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace, normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.chainTopCoeff_zero_right, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainLength_zero_right, LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace, LieAlgebra.Basis.borelUpper_le_biSup, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.mem_corootSpace', LieAlgebra.IsKilling.lieIdealOrderIso_right_inv, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.Basis.borelLower_eq, LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieAlgebra.IsKilling.chainBotCoeff_zero_right, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot, LieAlgebra.Basis.root_mem_or_mem_neg, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.rootSpace_two_smul, LieAlgebra.mem_corootSpace, LieIdeal.corootSubmodule_le, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieAlgebra.IsKilling.span_weight_eq_top, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left, LieAlgebra.Basis.coe_linearMap_baseSupp', LieModule.Weight.toLinear_neg, LieSubmodule.restr_toSubmodule, LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.Basis.coe_baseSupportEquiv_apply, LieAlgebra.rootSpaceProduct_tmul, LieIdeal.root_apply_eq_zero_of_notMem_rootSet, LieAlgebra.IsKilling.rootSystem_root_apply, LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule, LieAlgebra.IsKilling.lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, normalizer_eq_self_of_isCartanSubalgebra, LieModule.Weight.coe_neg, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple
lieSpan 📖	CompOp	20 math math: isLieAbelian_lieSpan_iff, submodule_span_le_lieSpan, span_univ, span_union, lieSpan_neg, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, lieSpan_mono, span_empty, subset_lieSpan, LieDerivation.eqOn_lieSpan, coe_lieSpan_eq_span_of_forall_lie_eq_zero, LieAlgebra.Basis.span_ef, lieSpan_le, coe_lieSpan_submodule_eq_iff, span_iUnion, lieSpan_eq, LieAlgebra.Basis.cartan_eq_lieSpan, mem_lieSpan, lieSpan_lieSpan_coe_preimage, comap_lieSpan_range_eq
map 📖	CompOp	6 math math: mem_map_submodule, map_le_iff_le_comap, LieEquiv.lieSubalgebraMap_apply, LieHom.range_eq_map, mem_map, gc_map_comap
ofLe 📖	CompOp	6 math math: equivOfLe_apply, mem_ofLe, exists_nested_lieIdeal_coe_eq_iff, coe_ofLe, exists_nested_lieIdeal_ofLe_normalizer, ofLe_eq_comap_incl
toSubmodule 📖	CompOp	45 math math: LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, top_toSubmodule, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, LieIdeal.restrict_killingForm, mem_map_submodule, submodule_span_le_lieSpan, LieAlgebra.coe_zeroRootSubalgebra, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, LieAlgebra.InvariantForm.restrict_nondegenerate, LieIdeal.coe_killingCompl_top, LieSubmodule.traceForm_eq_of_le_idealizer, toSubmodule_le_toSubmodule, mem_toSubmodule, mem_carrier, LieIdeal.incl_coe, LieAlgebra.Basis.coe_cartan_eq_span, coe_normalizer_eq_normalizer, coe_toSubmodule, sInf_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule, LieDerivation.IsKilling.killingForm_restrict_range_ad, toSubmodule_inj, toSubmodule_injective, LieDerivation.IsKilling.ad_mem_orthogonal_of_mem_orthogonal, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, coe_lieSpan_eq_span_of_forall_lie_eq_zero, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieAlgebra.InvariantForm.restrict_orthogonal_nondegenerate, toSubmodule_eq_bot, coe_ofLe, LieIdeal.killingForm_eq, disjoint_toSubmodule, LieAlgebra.restrict_killingForm, coe_toLieSubmodule, LieHom.range_toSubmodule, toSubmodule_eq_top, toSubmodule_mk, inf_toSubmodule, Submodule.exists_lieSubalgebra_coe_eq_iff, coe_lieSpan_submodule_eq_iff, LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra, bot_toSubmodule, LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, lie_mem_sup_of_mem_normalizer, lie_mem'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_sup 📖	mathematical	—	LieSubalgebra instAdd SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	—
add_mem 📖	mathematical	LieSubalgebra SetLike.instMembership instSetLike	LieSubalgebra SetLike.instMembership instSetLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup	—	AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass
bot_coe 📖	mathematical	—	SetLike.coe LieSubalgebra instSetLike Bot.bot instBot Set Set.instSingletonSet NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	—
bot_toSubmodule 📖	mathematical	—	toSubmodule Bot.bot LieSubalgebra instBot Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.instBot	—	—
coe_bracket 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike Bracket.bracket LieRingModule.toBracket lieRing LieRing.toAddCommGroup lieRingSelfModule	—	—
coe_bracket_of_module 📖	mathematical	—	Bracket.bracket LieSubalgebra SetLike.instMembership instSetLike instBracketSubtypeMem LieRingModule.toBracket	—	—
coe_incl 📖	mathematical	—	DFunLike.coe LieHom LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra LieHom.instFunLike incl	—	—
coe_incl' 📖	mathematical	—	DFunLike.coe LieModuleHom LieSubalgebra SetLike.instMembership instSetLike lieRing LieRing.toAddCommGroup instModuleSubtypeMemOfIsScalarTower CommSemiring.toSemiring CommRing.toCommSemiring Algebra.toSMul Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid Module.toDistribMulAction lieRingSelfModule lieRingModule LieModuleHom.instFunLike incl'	—	IsScalarTower.left
coe_inclusion 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	LieSubalgebra SetLike.instMembership instSetLike DFunLike.coe LieHom lieRing lieAlgebra LieHom.instFunLike inclusion	—	—
coe_inf 📖	mathematical	—	SetLike.coe LieSubalgebra instSetLike instMin Set Set.instInter	—	—
coe_injective 📖	mathematical	—	LieSubalgebra Set SetLike.coe instSetLike	—	SetLike.coe_injective
coe_lieSpan_eq_span_of_forall_lie_eq_zero 📖	mathematical	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	toSubmodule lieSpan Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule	—	Submodule.span_induction₂ AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass zero_lie lie_zero add_lie AddMemClass.add_mem AddSubmonoidClass.toAddMemClass lie_add smul_lie lieAlgebraSelfModule Submodule.smul_mem lie_smul le_antisymm lieSpan_le Submodule.subset_span submodule_span_le_lieSpan
coe_lieSpan_submodule_eq_iff 📖	mathematical	—	toSubmodule lieSpan SetLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.setLike LieSubalgebra	—	Submodule.exists_lieSubalgebra_coe_eq_iff mem_toSubmodule lie_mem subset_lieSpan coe_toSubmodule lieSpan_eq
coe_ofLe 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	toSubmodule LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra ofLe LinearMap.range Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.setLike Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.inclusion	—	—
coe_sInf 📖	mathematical	—	SetLike.coe LieSubalgebra instSetLike InfSet.sInf instInfSet Set.iInter Set Set.instMembership	—	coe_toSubmodule sInf_toSubmodule Submodule.coe_sInf Set.ext Set.iInter_exists Set.biInter_and' Set.iInter_congr_Prop Set.iInter_iInter_eq_right
coe_set_eq 📖	mathematical	—	SetLike.coe LieSubalgebra instSetLike	—	SetLike.coe_set_eq
coe_toSubmodule 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.setLike toSubmodule LieSubalgebra instSetLike	—	—
coe_zero_iff_zero 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup ZeroMemClass.zero AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass	—	AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass ext_iff
comap_lieSpan_range_eq 📖	mathematical	—	comap LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra incl lieSpan Set.range	—	le_antisymm lieSpan_induction subset_lieSpan Set.mem_range_self Subtype.coe_eta ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass smul_mem lie_mem lieSpan_le
disjoint_toSubmodule 📖	mathematical	—	Disjoint Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.instPartialOrder Submodule.instOrderBot toSubmodule LieSubalgebra instPartialOrder_1 BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder completeLattice	—	—
eq_bot_iff 📖	mathematical	—	Bot.bot LieSubalgebra instBot NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	eq_bot_iff
equivOfLe_apply 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	DFunLike.coe LieEquiv LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra ofLe EquivLike.toFunLike LieEquiv.instEquivLike equivOfLe LieHom LieHom.instFunLike inclusion LieHom.mem_range_self	—	—
ext 📖	—	LieSubalgebra SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike	—	—
ext_iff' 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike	—	SetLike.ext_iff
gc_map_comap 📖	mathematical	—	GaloisConnection LieSubalgebra PartialOrder.toPreorder instPartialOrder_1 map comap	—	map_le_iff_le_comap
incl_range 📖	mathematical	—	LieHom.range LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra incl	—	Submodule.range_subtype
inclusion_apply 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	DFunLike.coe LieHom LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra LieHom.instFunLike inclusion	—	—
inclusion_injective 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	LieSubalgebra SetLike.instMembership instSetLike DFunLike.coe LieHom lieRing lieAlgebra LieHom.instFunLike inclusion	—	—
inf_toSubmodule 📖	mathematical	—	toSubmodule LieSubalgebra instMin Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.instMin	—	—
instAddSubgroupClass 📖	mathematical	—	AddSubgroupClass LieSubalgebra AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup instSetLike	—	Submodule.add_mem AddSubmonoid.zero_mem' NegMemClass.neg_mem AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass
instCanonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd LieSubalgebra instAdd Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	—	sup_eq_right le_sup_right le_sup_left
instIsArtinianSubtypeMem 📖	mathematical	—	IsArtinian LieSubalgebra SetLike.instMembership instSetLike CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup lieRing instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	isArtinian_submodule'
instIsCentralScalarSubtypeMem 📖	mathematical	—	IsCentralScalar LieSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup lieRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleSubtypeMemOfIsScalarTower MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring	—	Submodule.isCentralScalar
instIsLieTowerSubtypeMem 📖	mathematical	—	IsLieTower LieSubalgebra SetLike.instMembership instSetLike instBracketSubtypeMem LieRing.toAddCommGroup lieRingSelfModule LieRingModule.toBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	leibniz_lie instIsLieTower
instIsNoetherianSubtypeMem 📖	mathematical	—	IsNoetherian LieSubalgebra SetLike.instMembership instSetLike CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup lieRing instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id LieAlgebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	isNoetherian_submodule'
instIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid LieSubalgebra addCommMonoid PartialOrder.toPreorder instPartialOrder_1	—	sup_le_sup_right
instIsScalarTowerSubtypeMem 📖	mathematical	—	IsScalarTower LieSubalgebra SetLike.instMembership instSetLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup lieRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Algebra.id LieAlgebra.toModule IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid	—	Submodule.isScalarTower
instSMulMemClass 📖	mathematical	—	SMulMemClass LieSubalgebra 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 instSetLike	—	SMulMemClass.smul_mem Submodule.smulMemClass
le_def 📖	mathematical	—	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1 Set Set.instHasSubset SetLike.coe instSetLike	—	—
lieModule 📖	mathematical	—	LieModule LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra lieRingModule	—	coe_bracket_of_module Submodule.coe_smul_of_tower smul_lie lie_smul
lieSpan_eq 📖	mathematical	—	lieSpan SetLike.coe LieSubalgebra instSetLike	—	le_antisymm lieSpan_le Eq.subset Set.instReflSubset subset_lieSpan
lieSpan_induction 📖	—	subset_lieSpan NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup zero_mem lieSpan AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid add_mem SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction LieAlgebra.toModule smul_mem Bracket.bracket LieRingModule.toBracket lieRingSelfModule lie_mem LieSubalgebra SetLike.instMembership instSetLike	—	—	subset_lieSpan zero_mem add_mem smul_mem lie_mem lieSpan_le
lieSpan_le 📖	mathematical	—	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1 lieSpan Set Set.instHasSubset SetLike.coe instSetLike	—	Set.Subset.trans subset_lieSpan mem_lieSpan
lieSpan_lieSpan_coe_preimage 📖	mathematical	—	lieSpan LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra Set.preimage Top.top instTop	—	eq_top_iff lieSpan_induction subset_lieSpan ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass smul_mem lie_mem
lieSpan_mono 📖	mathematical	Set Set.instHasSubset	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1 lieSpan	—	lieSpan_le Set.Subset.trans subset_lieSpan
lieSpan_neg 📖	mathematical	—	lieSpan Set InvolutiveNeg.toNeg Set.involutiveNeg SubtractionMonoid.toInvolutiveNeg SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	lieSpan_induction neg_mem_iff AddSubgroupClass.toNegMemClass instAddSubgroupClass subset_lieSpan Set.mem_neg ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SMulMemClass.smul_mem instSMulMemClass lie_mem le_antisymm neg_neg
lie_mem 📖	mathematical	LieSubalgebra SetLike.instMembership instSetLike	LieSubalgebra SetLike.instMembership instSetLike Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule	—	lie_mem'
lie_mem' 📖	mathematical	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid CommSemiring.toSemiring CommRing.toCommSemiring LieAlgebra.toModule toSubmodule	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid CommSemiring.toSemiring CommRing.toCommSemiring LieAlgebra.toModule toSubmodule Bracket.bracket LieRingModule.toBracket lieRingSelfModule	—	—
map_le_iff_le_comap 📖	mathematical	—	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1 map comap	—	Set.image_subset_iff
mem_bot 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike Bot.bot instBot NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	Set.mem_singleton_iff
mem_carrier 📖	mathematical	—	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid CommSemiring.toSemiring CommRing.toCommSemiring LieAlgebra.toModule toSubmodule SetLike.coe LieSubalgebra instSetLike	—	—
mem_coe 📖	mathematical	—	Set Set.instMembership SetLike.coe LieSubalgebra instSetLike SetLike.instMembership	—	—
mem_comap 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike comap DFunLike.coe LieHom LieHom.instFunLike	—	—
mem_inf 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike instMin	—	mem_toSubmodule inf_toSubmodule Submodule.mem_inf
mem_lieSpan 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike lieSpan	—	SetLike.mem_coe lieSpan.eq_1 coe_sInf Set.mem_iInter₂
mem_map 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike map DFunLike.coe LieHom LieHom.instFunLike	—	Submodule.mem_map RingHomSurjective.ids
mem_map_submodule 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike map LieEquiv.toLieHom Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.setLike Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LieEquiv.toLinearEquiv toSubmodule	—	—
mem_mk_iff 📖	mathematical	Set Set.instMembership AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddZero.toZero AddSubsemigroup.carrier AddSubmonoid.toAddSubsemigroup SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction LieAlgebra.toModule Submodule.toAddSubmonoid Bracket.bracket LieRingModule.toBracket lieRingSelfModule	LieSubalgebra SetLike.instMembership instSetLike CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toAdd AddZeroClass.toAddZero Set Set.instMembership	—	—
mem_mk_iff' 📖	mathematical	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid CommSemiring.toSemiring CommRing.toCommSemiring LieAlgebra.toModule Bracket.bracket LieRingModule.toBracket lieRingSelfModule	LieSubalgebra SetLike.instMembership instSetLike Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.setLike	—	—
mem_ofLe 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra ofLe	—	—
mem_toSubmodule 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule SetLike.instMembership Submodule.setLike toSubmodule LieSubalgebra instSetLike	—	—
mem_top 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike Top.top instTop	—	Set.mem_univ
mk_coe 📖	mathematical	Set Set.instMembership AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddZero.toZero AddSubsemigroup.carrier AddSubmonoid.toAddSubsemigroup SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction LieAlgebra.toModule Submodule.toAddSubmonoid Bracket.bracket LieRingModule.toBracket lieRingSelfModule	SetLike.coe LieSubalgebra instSetLike CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toAdd AddZeroClass.toAddZero	—	—
ofLe_eq_comap_incl 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	ofLe comap LieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra incl	—	ext mem_ofLe
sInf_glb 📖	mathematical	—	IsGLB LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1 InfSet.sInf instInfSet	—	IsGLB.of_image coe_sInf isGLB_biInf
sInf_toSubmodule 📖	mathematical	—	toSubmodule InfSet.sInf LieSubalgebra instInfSet Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.instInfSet setOf Set Set.instMembership	—	—
smul_mem 📖	mathematical	LieSubalgebra SetLike.instMembership instSetLike	LieSubalgebra SetLike.instMembership instSetLike 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	—	SMulMemClass.smul_mem instSMulMemClass
span_empty 📖	mathematical	—	lieSpan Set Set.instEmptyCollection Bot.bot LieSubalgebra instBot	—	GaloisConnection.l_bot GaloisInsertion.gc
span_iUnion 📖	mathematical	—	lieSpan Set.iUnion iSup LieSubalgebra ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	GaloisConnection.l_iSup GaloisInsertion.gc
span_union 📖	mathematical	—	lieSpan Set Set.instUnion LieSubalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	GaloisConnection.l_sup GaloisInsertion.gc
span_univ 📖	mathematical	—	lieSpan Set.univ Top.top LieSubalgebra instTop	—	eq_top_iff SetLike.le_def instIsConcreteLE subset_lieSpan
sub_mem 📖	mathematical	LieSubalgebra SetLike.instMembership instSetLike	LieSubalgebra SetLike.instMembership instSetLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup	—	sub_mem instAddSubgroupClass
submodule_span_le_lieSpan 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.span toSubmodule lieSpan	—	Submodule.span_le coe_toSubmodule subset_lieSpan
subset_lieSpan 📖	mathematical	—	Set Set.instHasSubset SetLike.coe LieSubalgebra instSetLike lieSpan	—	SetLike.mem_coe mem_lieSpan
subsingleton_bot 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike Bot.bot instBot	—	—
subsingleton_of_bot 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike Bot.bot instBot lieRing lieAlgebra	—	subsingleton_of_bot_eq_top ext mem_bot
toSubmodule_eq_bot 📖	mathematical	—	toSubmodule Bot.bot Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.instBot LieSubalgebra instBot	—	—
toSubmodule_eq_top 📖	mathematical	—	toSubmodule Top.top Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.instTop LieSubalgebra instTop	—	—
toSubmodule_inj 📖	mathematical	—	toSubmodule	—	toSubmodule_injective
toSubmodule_injective 📖	mathematical	—	LieSubalgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule toSubmodule	—	coe_set_eq SetLike.ext'_iff
toSubmodule_le_toSubmodule 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder toSubmodule LieSubalgebra instPartialOrder_1	—	—
toSubmodule_mk 📖	mathematical	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddSubmonoid.toAddSubsemigroup Submodule.toAddSubmonoid CommSemiring.toSemiring CommRing.toCommSemiring LieAlgebra.toModule Bracket.bracket LieRingModule.toBracket lieRingSelfModule	toSubmodule	—	—
top_coe 📖	mathematical	—	SetLike.coe LieSubalgebra instSetLike Top.top instTop Set.univ	—	—
top_toSubmodule 📖	mathematical	—	toSubmodule Top.top LieSubalgebra instTop Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule Submodule.instTop	—	—
wellFoundedGT_of_noetherian 📖	mathematical	—	WellFoundedGT LieSubalgebra Preorder.toLT PartialOrder.toPreorder instPartialOrder_1	—	RelHomClass.isWellFounded RelHom.instRelHomClass wellFoundedGT
zero_mem 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lieSubalgebra_coe_eq_iff 📖	mathematical	—	LieSubalgebra LieSubalgebra.toSubmodule Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule SetLike.instMembership setLike Bracket.bracket LieRingModule.toBracket lieRingSelfModule	—	LieSubalgebra.lie_mem'

(root)

Definitions

Name	Category	Theorems
LieSubalgebra 📖	CompData	339 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, LieSubalgebra.top_toSubmodule, RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieModule.Weight.IsZero.neg, LieDerivation.IsKilling.instIsKilling_range_ad, LieSubalgebra.inclusion_apply, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, LieSubalgebra.isLieAbelian_lieSpan_iff, skewAdjointMatricesLieSubalgebraEquivTranspose_apply, RootPairing.GeckConstruction.instHasTrivialRadical, LieAlgebra.Orthogonal.mem_so, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, LieHom.surjective_rangeRestrict, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, LieSubalgebra.le_normalizer, LieAlgebra.finrank_engel, skewAdjointLieSubalgebraEquiv_apply, LieSubalgebra.mem_map_submodule, LieSubalgebra.equivOfLe_apply, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, LieIdeal.reflectionPerm_mem_rootSet_iff, LieAlgebra.Basis.borelLower_le_biSup, LieModule.Weight.IsNonZero.neg, LieSubalgebra.toEnd_eq, LieAlgebra.coe_zeroRootSubalgebra, LieSubalgebra.span_univ, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, LieSubalgebra.subsingleton_bot, LieModule.isNilpotent_of_top_iff, LieSubalgebra.bot_coe, LieSubalgebra.span_union, LieAlgebra.Basis.symm_h', LieSubalgebra.mem_ofLe, skewAdjointLieSubalgebraEquiv_symm_apply, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, LieSubalgebra.mem_bot, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieAlgebra.IsKilling.reflectRoot_isNonZero, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieAlgebra.IsKilling.chainLength_nsmul, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieIdeal.toInvtRootSubmodule_mono, LieHom.equivRangeOfInjective_apply, LieHom.mem_range_self, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right, LieModule.isNilpotent_range_toEnd_iff, LieSubalgebra.toSubmodule_le_toSubmodule, LieAlgebra.Basis.cartan_eq, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieIdeal.coe_toLieSubalgebra, LieHom.isNilpotent_range, LieSubalgebra.IsCartanSubalgebra.nilpotent, LieSubalgebra.mem_toSubmodule, LieSubalgebra.mem_carrier, LieSubalgebra.lieSpan_mono, LieAlgebra.Basis.borelUpper_eq, LieAlgebra.Basis.linearIndepOn_root_baseSupp, LieSubalgebra.engel_carrier, LieSubalgebra.coe_injective, LieIdeal.rootSpan_mem_invtRootSubmodule, LieAlgebra.Basis.coroot_eq_h', LieSubalgebra.isNonZero_coe_root, LieModule.traceForm_lieSubalgebra_mk_right, LieAlgebra.IsKilling.chainLength_zero, LieSubalgebra.incl_range, LieSubalgebra.ideal_in_normalizer, LieSubalgebra.toEnd_mk, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.Basis.symm_baseSupp, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', IsSl2Triple.mem_toLieSubalgebra_iff, LieAlgebra.mem_biSup_genWeightSpace_of, LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff, LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop, LieSubalgebra.coe_bracket_of_module, LieAlgebra.Basis.baseSupp_apply_smul_f, LieSubalgebra.coe_normalizer_eq_normalizer, LieModule.exists_forall_mem_corootSpace_smul_add_eq_zero, LieSubalgebra.coe_toSubmodule, LieSubalgebra.sInf_toSubmodule, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, LieSubalgebra.coe_ad_pow, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieSubalgebra.subsingleton_of_bot, LieSubalgebra.add_mem, LieSubalgebra.mem_toLieSubmodule, LieSubalgebra.self_mem_engel, LieAlgebra.exists_engelian_lieSubalgebra_of_lt_normalizer, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieDerivation.IsKilling.killingForm_restrict_range_ad, LieSubalgebra.coe_inclusion, Derivation.Compatible.mem, LieEquiv.ofEq_apply, LieAlgebra.IsKilling.chainLength_neg, LieSubmodule.mem_restr, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, RootPairing.GeckConstruction.span_range_h'_eq_top, LieAlgebra.Basis.instIsLieAbelianSubtypeMemLieSubalgebraCartan, LieSubalgebra.coe_sInf, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieEquiv.ofSubalgebras_apply, LieSubalgebra.coe_set_eq, LieSubalgebra.toSubmodule_injective, LieModuleHom.coe_restrictLie, LieSubalgebra.map_le_iff_le_comap, LieAlgebra.Basis.iSupIndep_rootSpace, LieAlgebra.IsKilling.apply_coroot_eq_cast, LieSubalgebra.coe_incl', LieSubalgebra.span_empty, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', RootPairing.GeckConstruction.basis_A_eq, IsSl2Triple.h_eq_coroot, LieIdeal.restr_eq_iSup_sl2SubmoduleOfRoot, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.isSimple_iff_isIrreducible, LieHom.rangeRestrict_apply, LieAlgebra.SpecialLinear.sl_bracket, LieAlgebra.lieIdeal_eq_iSup_inf_genWeightSpace, LieSubalgebra.subset_lieSpan, LieHom.coe_range, LieModule.Weight.isZero_neg, instIsNilpotentSubtypeMemLieSubalgebraTop, LieSubalgebra.mem_comap, LieSubmodule.map_restrictLie_incl_top, LieSubalgebra.mem_inf, LieEquiv.lieSubalgebraMap_apply, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieAlgebra.IsKilling.rootSpace_one_div_two_smul, LieAlgebra.rootSpace_zero_eq, LieDerivation.eqOn_lieSpan, mem_skewAdjointMatricesLieSubalgebra, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, LieSubalgebra.lieModule, LieIdeal.mem_rootSet_of_mem_rootSpan, LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet, LieHom.range_eq_top, RootPairing.GeckConstruction.instIsIrreducible, LieSubalgebra.mem_engel_iff, LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra, LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule, Derivation.Compatible.apply, LieHom.range_eq_map, LieSubalgebra.isNilpotent_of_forall_le_engel, LieSubalgebra.instCanonicallyOrderedAdd, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LieSubalgebra.instIsLieTowerSubtypeMem, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, LieSubalgebra.coe_bracket, LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieAlgebra.toEnd_pow_apply_mem, LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace, LieModule.coe_genWeightSpace_of_top, LieIdeal.mem_rootSet, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, LieAlgebra.Basis.baseSupp_apply_smul_e, LieHom.quotKerEquivRange_invFun, LieSubalgebra.toSubmodule_eq_bot, LieSubalgebra.top_coe, LieSubalgebra.coe_ofLe, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, LieSubalgebra.inclusion_injective, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit, RootPairing.GeckConstruction.h_mem_cartanSubalgebra', LieAlgebra.rootSpace_comap_eq_genWeightSpace, LieModule.traceForm_lieSubalgebra_mk_left, LieSubalgebra.disjoint_toSubmodule, LieIdeal.rootSpace_le_of_apply_coroot_ne_zero, LieSubalgebra.ext_iff', LieAlgebra.restrict_killingForm, mem_skewAdjointMatricesLieSubalgebra_unit_smul, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra, LieAlgebra.IsKilling.root_apply_coroot, LieAlgebra.IsKilling.coroot_neg, LieSubalgebra.mem_normalizer_iff', LieHom.idealRange_eq_lieSpan_range, LieSubalgebra.coe_inf, LieAlgebra.Basis.span_ef, LieAlgebra.SpecialLinear.val_single, LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_corootSpace, LieSubalgebra.instIsNoetherianSubtypeMem, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, LieSubalgebra.engel_zero, LieIdeal.mem_toLieSubalgebra, LieAlgebra.Basis.cartanMatrix_base_eq, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, RootPairing.GeckConstruction.h_mem_lieAlgebra, LieSubalgebra.exists_lieIdeal_coe_eq_iff, LieAlgebra.rank_le_finrank_engel, LieSubalgebra.topEquiv_apply, LieDerivation.IsKilling.range_ad_eq_top, LieSubalgebra.instNontrivialSubtypeMemOfIsCartanSubalgebra, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.eq_neg_or_eq_of_eq_smul, LieAlgebra.lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace, LieHom.isSolvable_range, LieSubalgebra.normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.chainTopCoeff_zero_right, LieSubalgebra.coe_incl, LieSubalgebra.ext_iff, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieSubalgebra.lieSpan_le, LieSubalgebra.toSubmodule_eq_top, LieIdeal.normalizer_eq_top, LieSubalgebra.mk_coe, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, LieAlgebra.top_isCartanSubalgebra_of_nilpotent, LieHom.range_subset_idealRange, LieEquiv.ofSubalgebras_symm_apply, LieSubalgebra.coe_zero_iff_zero, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, RootPairing.GeckConstruction.ωConj_mem_of_mem, LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainLength_zero_right, LieAlgebra.IsKilling.chainLength_smul, LieEquiv.ofInjective_apply, LieSubalgebra.inf_toSubmodule, LieSubalgebra.sub_mem, LieIdeal.top_toLieSubalgebra, Submodule.exists_lieSubalgebra_coe_eq_iff, LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace, LieAlgebra.Basis.borelUpper_le_biSup, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieSubalgebra.instIsOrderedAddMonoid, LieAlgebra.mem_corootSpace', LieSubalgebra.mem_map, LieAlgebra.IsKilling.lieIdealOrderIso_right_inv, LieSubalgebra.zero_mem, LieAlgebra.eq_rootSpace_zero_iff_isCartan, LieAlgebra.isNilpotent_range_ad_iff, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.Basis.borelLower_eq, LieAlgebra.IsExtension.range_eq_top, LieSubalgebra.mem_mk_iff', LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieSubalgebra.coe_lieSpan_submodule_eq_iff, LieAlgebra.IsKilling.chainBotCoeff_zero_right, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer, LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot, LieSubalgebra.span_iUnion, LieAlgebra.Basis.root_mem_or_mem_neg, LieHom.mem_range, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.rootSpace_two_smul, LieAlgebra.isRegular_iff_finrank_engel_eq_rank, LieSubalgebra.instIsScalarTowerSubtypeMem, LieSubalgebra.wellFoundedGT_of_noetherian, LieSubalgebra.mem_coe, LieAlgebra.mem_corootSpace, RootPairing.GeckConstruction.f_mem_lieAlgebra, LieIdeal.corootSubmodule_le, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, RootPairing.GeckConstruction.e_mem_lieAlgebra, LieAlgebra.SpecialLinear.val_singleSubSingle, LieSubalgebra.lieSpan_eq, LieAlgebra.IsKilling.span_weight_eq_top, LieSubalgebra.bot_toSubmodule, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left, skewAdjointMatricesLieSubalgebraEquiv_apply, LieSubalgebra.le_def, LieAlgebra.Basis.coe_linearMap_baseSupp', LieAlgebra.isNilpotent_ad_of_isNilpotent, LieModule.Weight.toLinear_neg, LieSubalgebra.add_eq_sup, Derivation.Compatible.mk_left, LieSubmodule.restr_toSubmodule, LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, LieSubalgebra.mem_lieSpan, LieSubalgebra.mem_top, LieSubalgebra.ofLe_eq_comap_incl, LieSubalgebra.instSMulMemClass, LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.Basis.coe_baseSupportEquiv_apply, LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff, LieAlgebra.Basis.linearIndependent_baseSupp, LieSubalgebra.instIsCentralScalarSubtypeMem, LieSubalgebra.sInf_glb, LieAlgebra.le_zeroRootSubalgebra, LieSubalgebra.lieSpan_lieSpan_coe_preimage, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieAlgebra.rootSpaceProduct_tmul, LieSubalgebra.mem_normalizer_iff, LieIdeal.root_apply_eq_zero_of_notMem_rootSet, LieAlgebra.Basis.baseSupp_apply_h', LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.IsKilling.rootSystem_root_apply, LieAlgebra.IsKilling.coe_coroot_mem_corootSubmodule, LieAlgebra.IsKilling.lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, LieSubalgebra.instIsArtinianSubtypeMem, Derivation.Compatible.mk_right, LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra, LieSubalgebra.smul_mem, LieModule.Weight.coe_neg, LieSubalgebra.gc_map_comap, LieSubalgebra.eq_bot_iff, LieSubalgebra.mem_mk_iff, LieSubalgebra.instAddSubgroupClass, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, LieSubalgebra.coe_ad, LieSubalgebra.lie_mem, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, LieSubalgebra.comap_lieSpan_range_eq, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra, LieAlgebra.engel_isBot_of_isMin, LieSubalgebra.ad_comp_incl_eq
instCoeLieSubalgebraSubmodule 📖	CompOp	—
instInhabitedLieSubalgebra 📖	CompOp	—
instZeroLieSubalgebra 📖	CompOp	—

---

← Back to Index