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_coe, 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, eq_bot_iff, equivOfLe_apply, ext, ext_iff, ext_iff', gc_map_comap, incl_range, inclusion_apply, inclusion_injective, inf_coe, inf_toSubmodule, instAddSubgroupClass, instCanonicallyOrderedAdd, instIsArtinianSubtypeMem, instIsCentralScalarSubtypeMem, instIsLieTowerSubtypeMem, instIsNoetherianSubtypeMem, instIsOrderedAddMonoid, instIsScalarTowerSubtypeMem, instSMulMemClass, le_def, lieModule, lieSpan_eq, lieSpan_induction, lieSpan_le, lieSpan_mono, 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_coe, 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	100
Total	138

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	SetLike.instMembership 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 LieEquiv LieSubalgebra.lieRing LieSubalgebra.lieAlgebra EquivLike.toFunLike instEquivLike ofInjective	—	—
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	32 math math: 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, rangeRestrict_apply, coe_range, range_eq_top, range_eq_map, range_coe, quotKerEquivRange_invFun, idealRange_eq_lieSpan_range, LieDerivation.IsKilling.range_ad_eq_top, range_toSubmodule, isSolvable_range, 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	LieEquiv LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike range LieSubalgebra.lieRing LieSubalgebra.lieAlgebra EquivLike.toFunLike LieEquiv.instEquivLike equivRangeOfInjective 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_coe 📖	mathematical	—	SetLike.coe LieSubalgebra LieSubalgebra.instSetLike range Set.range DFunLike.coe LieHom instFunLike	—	coe_range
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	1 math math: coe_restrictLie

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	4 math math: map_le_iff_le_comap, mem_comap, ofLe_eq_comap_incl, gc_map_comap
completeLattice 📖	CompOp	3 math math: span_union, span_iUnion, add_eq_sup
equivOfLe 📖	CompOp	1 math math: equivOfLe_apply
gi 📖	CompOp	—
incl 📖	CompOp	5 math math: incl_range, LieModule.coe_genWeightSpace_of_top, coe_incl, ofLe_eq_comap_incl, 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	5 math math: LieAlgebra.IsKilling.chainLength_nsmul, coe_bracket_of_module, instIsLieTowerSubtypeMem, LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace, LieAlgebra.IsKilling.chainLength_smul
instInfSet 📖	CompOp	4 math math: sInf_coe, sInf_toSubmodule, coe_sInf, sInf_glb
instMin 📖	CompOp	4 math math: inf_coe, mem_inf, coe_inf, inf_toSubmodule
instModuleSubtypeMemOfIsScalarTower 📖	CompOp	33 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieAlgebra.finrank_engel, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, RootPairing.GeckConstruction.span_range_h'_eq_top, coe_incl', LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, 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.rootSpace_comap_eq_genWeightSpace, LieAlgebra.SpecialLinear.val_single, instIsNoetherianSubtypeMem, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, LieAlgebra.rank_le_finrank_engel, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieAlgebra.mem_corootSpace', LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.isRegular_iff_finrank_engel_eq_rank, instIsScalarTowerSubtypeMem, LieAlgebra.SpecialLinear.val_singleSubSingle, instIsCentralScalarSubtypeMem, 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	13 math math: le_normalizer, toSubmodule_le_toSubmodule, lieSpan_mono, map_le_iff_le_comap, instCanonicallyOrderedAdd, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, lieSpan_le, instIsOrderedAddMonoid, wellFoundedGT_of_noetherian, le_def, sInf_glb, LieAlgebra.le_zeroRootSubalgebra, gc_map_comap
instSetLike 📖	CompOp	201 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, 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.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, toEnd_eq, LieAlgebra.coe_zeroRootSubalgebra, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, subsingleton_bot, LieModule.isNilpotent_of_top_iff, bot_coe, mem_ofLe, skewAdjointLieSubalgebraEquiv_symm_apply, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, mem_bot, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieHom.equivRangeOfInjective_apply, LieHom.mem_range_self, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, LieModule.isNilpotent_range_toEnd_iff, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieIdeal.coe_toLieSubalgebra, LieHom.isNilpotent_range, IsCartanSubalgebra.nilpotent, mem_toSubmodule, mem_carrier, engel_carrier, coe_injective, LieAlgebra.IsKilling.chainLength_zero, incl_range, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', IsSl2Triple.mem_toLieSubalgebra_iff, sInf_coe, exists_nested_lieIdeal_coe_eq_iff, LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop, coe_bracket_of_module, inf_coe, 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, mem_toLieSubmodule, self_mem_engel, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieDerivation.IsKilling.killingForm_restrict_range_ad, coe_inclusion, LieAlgebra.IsKilling.chainLength_neg, RootPairing.GeckConstruction.span_range_h'_eq_top, coe_sInf, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieEquiv.ofSubalgebras_apply, coe_set_eq, LieModuleHom.coe_restrictLie, LieAlgebra.IsKilling.apply_coroot_eq_cast, coe_incl', RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieHom.rangeRestrict_apply, LieAlgebra.SpecialLinear.sl_bracket, subset_lieSpan, LieHom.coe_range, LieModule.Weight.isZero_neg, instIsNilpotentSubtypeMemLieSubalgebraTop, mem_comap, mem_inf, LieEquiv.lieSubalgebraMap_apply, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieAlgebra.rootSpace_zero_eq, LieDerivation.eqOn_lieSpan, mem_skewAdjointMatricesLieSubalgebra, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, lieModule, RootPairing.GeckConstruction.instIsIrreducible, mem_engel_iff, ucs_eq_self_of_isCartanSubalgebra, LieHom.range_coe, isNilpotent_of_forall_le_engel, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, instIsLieTowerSubtypeMem, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, coe_bracket, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieModule.coe_genWeightSpace_of_top, 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, LieAlgebra.rootSpace_comap_eq_genWeightSpace, ext_iff', LieAlgebra.restrict_killingForm, mem_skewAdjointMatricesLieSubalgebra_unit_smul, coe_toLieSubmodule, instIsNilpotentSubtypeMemOfIsCartanSubalgebra, LieAlgebra.IsKilling.coroot_neg, mem_normalizer_iff', LieHom.idealRange_eq_lieSpan_range, coe_inf, LieAlgebra.SpecialLinear.val_single, instIsNoetherianSubtypeMem, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, 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, LieHom.isSolvable_range, normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, 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, LieHom.range_subset_idealRange, LieEquiv.ofSubalgebras_symm_apply, coe_zero_iff_zero, LieEquiv.ofInjective_apply, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.mem_corootSpace', mem_map, zero_mem, LieAlgebra.isNilpotent_range_ad_iff, LieAlgebra.IsKilling.traceForm_coroot, mem_mk_iff', LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, exists_nested_lieIdeal_ofLe_normalizer, LieHom.mem_range, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.isRegular_iff_finrank_engel_eq_rank, instIsScalarTowerSubtypeMem, mem_coe, LieAlgebra.mem_corootSpace, RootPairing.GeckConstruction.f_mem_lieAlgebra, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, RootPairing.GeckConstruction.e_mem_lieAlgebra, LieAlgebra.SpecialLinear.val_singleSubSingle, lieSpan_eq, LieAlgebra.IsKilling.span_weight_eq_top, skewAdjointMatricesLieSubalgebraEquiv_apply, le_def, LieModule.Weight.toLinear_neg, mem_lieSpan, mem_top, ofLe_eq_comap_incl, instSMulMemClass, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, instIsCentralScalarSubtypeMem, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, mem_normalizer_iff, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.IsKilling.rootSystem_root_apply, instIsArtinianSubtypeMem, normalizer_eq_self_of_isCartanSubalgebra, LieModule.Weight.coe_neg, mem_mk_iff, instAddSubgroupClass, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, coe_ad, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra, ad_comp_incl_eq
instTop 📖	CompOp	20 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, 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
instZero 📖	CompOp	—
lieAlgebra 📖	CompOp	112 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, 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, toEnd_eq, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, mem_ofLe, skewAdjointLieSubalgebraEquiv_symm_apply, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieHom.equivRangeOfInjective_apply, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieModule.traceForm_lieSubalgebra_mk_right, LieAlgebra.IsKilling.chainLength_zero, incl_range, toEnd_mk, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', 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, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieDerivation.IsKilling.killingForm_restrict_range_ad, coe_inclusion, LieEquiv.ofEq_apply, LieAlgebra.IsKilling.chainLength_neg, RootPairing.GeckConstruction.span_range_h'_eq_top, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieEquiv.ofSubalgebras_apply, LieAlgebra.IsKilling.apply_coroot_eq_cast, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieHom.rangeRestrict_apply, LieModule.Weight.isZero_neg, LieEquiv.lieSubalgebraMap_apply, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, lieModule, ucs_eq_self_of_isCartanSubalgebra, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, isNilpotent_ad_of_isNilpotent_ad, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieModule.coe_genWeightSpace_of_top, 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.coroot_neg, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, topEquiv_apply, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, coe_incl, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieEquiv.ofSubalgebras_symm_apply, LieEquiv.ofInjective_apply, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.mem_corootSpace', LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.IsKilling.coroot_zero, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, exists_nested_lieIdeal_ofLe_normalizer, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.mem_corootSpace, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieAlgebra.IsKilling.span_weight_eq_top, skewAdjointMatricesLieSubalgebraEquiv_apply, LieAlgebra.isNilpotent_ad_of_isNilpotent, LieModule.Weight.toLinear_neg, ofLe_eq_comap_incl, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieAlgebra.rootSpaceProduct_tmul, LieAlgebra.IsKilling.rootSystem_root_apply, normalizer_eq_self_of_isCartanSubalgebra, LieModule.Weight.coe_neg, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, coe_ad, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, ad_comp_incl_eq
lieRing 📖	CompOp	150 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, 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.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, 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, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieHom.equivRangeOfInjective_apply, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, LieModule.isNilpotent_range_toEnd_iff, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieHom.isNilpotent_range, IsCartanSubalgebra.nilpotent, LieModule.traceForm_lieSubalgebra_mk_right, LieAlgebra.IsKilling.chainLength_zero, incl_range, toEnd_mk, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', exists_nested_lieIdeal_coe_eq_iff, LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop, coe_normalizer_eq_normalizer, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, coe_ad_pow, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, subsingleton_of_bot, mem_toLieSubmodule, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieDerivation.IsKilling.killingForm_restrict_range_ad, coe_inclusion, LieEquiv.ofEq_apply, LieAlgebra.IsKilling.chainLength_neg, RootPairing.GeckConstruction.span_range_h'_eq_top, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieEquiv.ofSubalgebras_apply, LieModuleHom.coe_restrictLie, LieAlgebra.IsKilling.apply_coroot_eq_cast, coe_incl', RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieHom.rangeRestrict_apply, LieAlgebra.SpecialLinear.sl_bracket, LieModule.Weight.isZero_neg, instIsNilpotentSubtypeMemLieSubalgebraTop, LieEquiv.lieSubalgebraMap_apply, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, lieModule, RootPairing.GeckConstruction.instIsIrreducible, ucs_eq_self_of_isCartanSubalgebra, isNilpotent_of_forall_le_engel, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, coe_bracket, isNilpotent_ad_of_isNilpotent_ad, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieModule.coe_genWeightSpace_of_top, 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, coe_toLieSubmodule, instIsNilpotentSubtypeMemOfIsCartanSubalgebra, LieAlgebra.IsKilling.coroot_neg, LieAlgebra.SpecialLinear.val_single, instIsNoetherianSubtypeMem, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, 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, LieHom.isSolvable_range, normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, coe_incl, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieEquiv.ofSubalgebras_symm_apply, LieEquiv.ofInjective_apply, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.mem_corootSpace', LieAlgebra.isNilpotent_range_ad_iff, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, exists_nested_lieIdeal_ofLe_normalizer, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.isRegular_iff_finrank_engel_eq_rank, instIsScalarTowerSubtypeMem, LieAlgebra.mem_corootSpace, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieAlgebra.SpecialLinear.val_singleSubSingle, LieAlgebra.IsKilling.span_weight_eq_top, skewAdjointMatricesLieSubalgebraEquiv_apply, LieAlgebra.isNilpotent_ad_of_isNilpotent, LieModule.Weight.toLinear_neg, ofLe_eq_comap_incl, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, instIsCentralScalarSubtypeMem, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieAlgebra.rootSpaceProduct_tmul, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.IsKilling.rootSystem_root_apply, instIsArtinianSubtypeMem, normalizer_eq_self_of_isCartanSubalgebra, LieModule.Weight.coe_neg, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, coe_ad, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra, ad_comp_incl_eq
lieRingModule 📖	CompOp	82 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, 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, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieModule.isNilpotent_range_toEnd_iff, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieModule.traceForm_lieSubalgebra_mk_right, LieAlgebra.IsKilling.chainLength_zero, toEnd_mk, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', 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, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieModuleHom.coe_restrictLie, LieAlgebra.IsKilling.apply_coroot_eq_cast, coe_incl', LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieModule.Weight.isZero_neg, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, lieModule, RootPairing.GeckConstruction.instIsIrreducible, ucs_eq_self_of_isCartanSubalgebra, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieModule.coe_genWeightSpace_of_top, 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, LieAlgebra.restrict_killingForm, coe_toLieSubmodule, LieAlgebra.IsKilling.coroot_neg, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.mem_corootSpace', LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.mem_corootSpace, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieAlgebra.IsKilling.span_weight_eq_top, LieModule.Weight.toLinear_neg, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.rootSpaceProduct_tmul, LieAlgebra.IsKilling.rootSystem_root_apply, normalizer_eq_self_of_isCartanSubalgebra, LieModule.Weight.coe_neg, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple
lieSpan 📖	CompOp	15 math math: isLieAbelian_lieSpan_iff, submodule_span_le_lieSpan, span_univ, span_union, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, lieSpan_mono, span_empty, subset_lieSpan, LieDerivation.eqOn_lieSpan, coe_lieSpan_eq_span_of_forall_lie_eq_zero, lieSpan_le, coe_lieSpan_submodule_eq_iff, span_iUnion, lieSpan_eq, mem_lieSpan
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	39 math math: 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, coe_normalizer_eq_normalizer, coe_toSubmodule, sInf_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule, LieDerivation.IsKilling.killingForm_restrict_range_ad, toSubmodule_inj, toSubmodule_injective, 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, 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

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	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	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 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	—	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 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
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 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 SetLike.instMembership instSetLike lieRing lieAlgebra LieHom.instFunLike inclusion	—	—
inclusion_injective 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	SetLike.instMembership instSetLike DFunLike.coe LieHom lieRing lieAlgebra LieHom.instFunLike inclusion	—	—
inf_coe 📖	mathematical	—	SetLike.coe LieSubalgebra instSetLike instMin Set Set.instInter	—	coe_inf
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 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 IsScalarTower.left 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_mono 📖	mathematical	Set Set.instHasSubset	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1 lieSpan	—	lieSpan_le Set.Subset.trans subset_lieSpan
lie_mem 📖	mathematical	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	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	—	—
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 Submodule.setLike	—	—
mem_ofLe 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	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	—	—
ofLe_eq_comap_incl 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	ofLe comap SetLike.instMembership instSetLike lieRing lieAlgebra incl	—	ext mem_ofLe
sInf_coe 📖	mathematical	—	SetLike.coe LieSubalgebra instSetLike InfSet.sInf instInfSet Set.iInter Set Set.instMembership	—	coe_sInf
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	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	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.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	223 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, LieDerivation.IsKilling.instIsKilling_range_ad, 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.IsKilling.isCompl_ker_weight_span_coroot, LieSubalgebra.le_normalizer, LieAlgebra.finrank_engel, skewAdjointLieSubalgebraEquiv_apply, LieSubalgebra.mem_map_submodule, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, 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, skewAdjointLieSubalgebraEquiv_symm_apply, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, LieSubalgebra.mem_bot, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieHom.equivRangeOfInjective_apply, LieHom.mem_range_self, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, LieModule.isNilpotent_range_toEnd_iff, LieSubalgebra.toSubmodule_le_toSubmodule, LieModule.instIsTriangularizableSubtypeMemLieSubalgebra, LieIdeal.coe_toLieSubalgebra, LieHom.isNilpotent_range, LieSubalgebra.IsCartanSubalgebra.nilpotent, LieSubalgebra.mem_toSubmodule, LieSubalgebra.mem_carrier, LieSubalgebra.lieSpan_mono, LieSubalgebra.engel_carrier, LieSubalgebra.coe_injective, LieAlgebra.IsKilling.chainLength_zero, LieSubalgebra.incl_range, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', IsSl2Triple.mem_toLieSubalgebra_iff, LieSubalgebra.sInf_coe, LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop, LieSubalgebra.coe_bracket_of_module, LieSubalgebra.inf_coe, 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.mem_toLieSubmodule, LieSubalgebra.self_mem_engel, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieDerivation.IsKilling.killingForm_restrict_range_ad, LieAlgebra.IsKilling.chainLength_neg, RootPairing.GeckConstruction.span_range_h'_eq_top, 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.IsKilling.apply_coroot_eq_cast, LieSubalgebra.coe_incl', LieSubalgebra.span_empty, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieHom.rangeRestrict_apply, LieAlgebra.SpecialLinear.sl_bracket, LieSubalgebra.subset_lieSpan, LieHom.coe_range, LieModule.Weight.isZero_neg, instIsNilpotentSubtypeMemLieSubalgebraTop, LieSubalgebra.mem_comap, LieSubalgebra.mem_inf, LieEquiv.lieSubalgebraMap_apply, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieAlgebra.rootSpace_zero_eq, LieDerivation.eqOn_lieSpan, mem_skewAdjointMatricesLieSubalgebra, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, LieSubalgebra.lieModule, LieHom.range_eq_top, RootPairing.GeckConstruction.instIsIrreducible, LieSubalgebra.mem_engel_iff, LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra, LieHom.range_eq_map, LieHom.range_coe, LieSubalgebra.instCanonicallyOrderedAdd, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, LieSubalgebra.instIsLieTowerSubtypeMem, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieSubalgebra.coe_bracket, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieModule.coe_genWeightSpace_of_top, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, LieHom.quotKerEquivRange_invFun, LieSubalgebra.toSubmodule_eq_bot, LieSubalgebra.top_coe, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit, LieAlgebra.rootSpace_comap_eq_genWeightSpace, LieSubalgebra.ext_iff', LieAlgebra.restrict_killingForm, mem_skewAdjointMatricesLieSubalgebra_unit_smul, LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.instIsNilpotentSubtypeMemOfIsCartanSubalgebra, LieAlgebra.IsKilling.coroot_neg, LieSubalgebra.mem_normalizer_iff', LieHom.idealRange_eq_lieSpan_range, LieSubalgebra.coe_inf, LieAlgebra.SpecialLinear.val_single, LieSubalgebra.instIsNoetherianSubtypeMem, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, LieSubalgebra.engel_zero, 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, LieHom.isSolvable_range, LieSubalgebra.normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, 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.top_isCartanSubalgebra_of_nilpotent, LieHom.range_subset_idealRange, LieEquiv.ofSubalgebras_symm_apply, LieSubalgebra.coe_zero_iff_zero, LieEquiv.ofInjective_apply, LieSubalgebra.inf_toSubmodule, LieIdeal.top_toLieSubalgebra, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieSubalgebra.instIsOrderedAddMonoid, LieAlgebra.mem_corootSpace', LieSubalgebra.mem_map, LieSubalgebra.zero_mem, LieAlgebra.isNilpotent_range_ad_iff, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.IsExtension.range_eq_top, LieSubalgebra.mem_mk_iff', LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieModule.Weight.isNonZero_neg, LieModule.instIsFaithfulSubtypeMemLieSubalgebra, LieSubalgebra.span_iUnion, LieHom.mem_range, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.isRegular_iff_finrank_engel_eq_rank, LieSubalgebra.instIsScalarTowerSubtypeMem, LieSubalgebra.wellFoundedGT_of_noetherian, LieSubalgebra.mem_coe, LieAlgebra.mem_corootSpace, RootPairing.GeckConstruction.f_mem_lieAlgebra, 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, skewAdjointMatricesLieSubalgebraEquiv_apply, LieSubalgebra.le_def, LieModule.Weight.toLinear_neg, LieSubalgebra.add_eq_sup, LieSubalgebra.mem_lieSpan, LieSubalgebra.mem_top, LieSubalgebra.instSMulMemClass, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieSubalgebra.instIsCentralScalarSubtypeMem, LieSubalgebra.sInf_glb, LieAlgebra.le_zeroRootSubalgebra, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieSubalgebra.mem_normalizer_iff, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.IsKilling.rootSystem_root_apply, LieSubalgebra.instIsArtinianSubtypeMem, LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra, 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, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra, LieSubalgebra.ad_comp_incl_eq
instCoeLieSubalgebraSubmodule 📖	CompOp	—
instInhabitedLieSubalgebra 📖	CompOp	—
instZeroLieSubalgebra 📖	CompOp	—

---

← Back to Index