| Metric | Count |
|---|
DefinitionsofTop, codRestrict, ker, range, toLieSubmodule, topEquiv, LieSubmodule, coeSort, coeSubmodule, comap, copy, equivMapOfInjective, gi, incl, inclusion, instAdd, instAddCommMonoid, instBot, instCompleteLattice, instInfSet, instInhabited, instLieRingModuleSubtypeMem, instMax, instMin, instPartialOrder, instSetLike, instSupSet, instTop, instUniqueBot, instUniqueOfSubsingleton, instZero, lieSpan, map, mapOrderEmbedding, orderIsoMapComap, toSubmodule, toSubmodule_orderEmbedding | 37 |
TheoremsofTop_apply, range_coe, codRestrict_apply, coe_range, comp_ker_incl, ker_eq_bot, ker_id, ker_toSubmodule, le_ker_iff_map, map_top, mem_ker, mem_range, range_eq_top, toSubmodule_range, coe_toLieSubmodule, mem_toLieSubmodule, topEquiv_apply, add_eq_sup, bot_coe, bot_toSubmodule, codisjoint_toSubmodule, coe_add, coe_bracket, coe_copy, coe_iInf, coe_inclusion, coe_inf, coe_injective, coe_lieSpan_submodule_eq_iff, coe_map, coe_neg, coe_sInf, coe_smul, coe_sub, coe_toSet_mk, coe_toSubmodule, coe_zero, comap_incl_eq_bot, comap_incl_eq_top, comap_incl_self, comap_inf, copy_eq, disjoint_toSubmodule, eq_bot_iff, ext, ext_iff, gc_map_comap, iInf_coe, iInf_toSubmodule, iSupIndep_toSubmodule, iSup_induction, iSup_induction', iSup_toSubmodule, iSup_toSubmodule_eq_top, incl_apply, incl_coe, incl_eq_val, inclusion_apply, inclusion_injective, inf_coe, inf_toSubmodule, injective_incl, instAddSubgroupClass, instCanLiftSubmoduleToSubmoduleForallForallForallMemBracket, instIsArtinianSubtypeMem, instIsAtomicOfIsArtinian, instIsCompactlyGenerated, instIsModularLattice, instIsNoetherianSubtypeMem, instIsTorsionFreeSubtypeMem, instLieModule, instNontrivial, instSMulMemClass, isCompactElement_lieSpan_singleton, isCompl_toSubmodule, ker_incl, lieSpan_eq, lieSpan_eq_bot_iff, lieSpan_induction, lieSpan_le, lieSpan_mono, lie_mem, mapOrderEmbedding_apply, map_bot, map_comp, map_iSup, map_id, map_incl_le, map_incl_lt_iff_lt_top, map_incl_top, map_inf, map_inf_le, map_injective_of_injective, map_le_iff_le_comap, map_le_map_iff, map_le_range, map_mono, map_sup, mem_bot, mem_carrier, mem_coe, mem_comap, mem_iInf, mem_iSup_of_mem, mem_inf, mem_lieSpan, mem_map, mem_map_of_mem, mem_mk_iff, mem_mk_iff', mem_sup, mem_toSubmodule, mem_top, mk_eq_bot_iff, mk_eq_top_iff, mk_eq_zero, nontrivial_iff, nontrivial_iff_ne_bot, orderIsoMapComap_apply, orderIsoMapComap_symm_apply, range_incl, sInf_coe, sInf_toSubmodule, sInf_toSubmodule_eq_iInf, sSup_image_lieSpan_singleton, sSup_toSubmodule, sSup_toSubmodule_eq_iSup, span_empty, span_iUnion, span_union, span_univ, submodule_span_le_lieSpan, subset_lieSpan, subsingleton_iff, subsingleton_of_bot, sup_toSubmodule, toSubmodule_comap, toSubmodule_eq_bot, toSubmodule_eq_top, toSubmodule_inj, toSubmodule_injective, toSubmodule_le_toSubmodule, toSubmodule_map, toSubmodule_mk, toSubmodule_orderEmbedding_apply, top_coe, top_toSubmodule, wellFoundedGT_of_noetherian, wellFoundedLT_of_isArtinian, zero_mem, exists_lieSubmodule_coe_eq_iff | 151 |
| Total | 188 |
| Name | Category | Theorems |
|---|
coeSort π | CompOp | β |
coeSubmodule π | CompOp | β |
comap π | CompOp | 20 mathmath: mem_comap, comap_bracket_eq, comap_incl_eq_top, comap_incl_eq_bot, ucs_comap_incl, orderIsoMapComap_symm_apply, map_comap_le, comap_map_eq, lowerCentralSeries_eq_lcs_comap, LieAlgebra.rootSpace_comap_eq_genWeightSpace, gc_map_comap, toSubmodule_comap, LieModule.comap_genWeightSpace_eq_of_injective, comap_normalizer, map_le_iff_le_comap, map_comap_eq, comap_inf, le_comap_map, map_comap_incl, comap_incl_self
|
copy π | CompOp | 2 mathmath: coe_copy, copy_eq
|
equivMapOfInjective π | CompOp | β |
gi π | CompOp | β |
incl π | CompOp | 20 mathmath: TensorProduct.LieModule.mapIncl_def, incl_apply, lowerCentralSeries_map_eq_lcs, map_incl_top, comap_incl_eq_top, comap_incl_eq_bot, ucs_comap_incl, range_incl, map_incl_lt_iff_lt_top, ker_incl, LieModuleHom.comp_ker_incl, map_incl_le, lowerCentralSeries_eq_lcs_comap, incl_eq_val, incl_coe, injective_incl, map_comap_incl, comap_incl_self, LieModule.posFittingComp_map_incl_sup_of_codisjoint, LieModule.genWeightSpace_genWeightSpaceOf_map_incl
|
inclusion π | CompOp | 3 mathmath: coe_inclusion, inclusion_apply, inclusion_injective
|
instAdd π | CompOp | 4 mathmath: LieAlgebra.derivedSeriesOfIdeal_add_le_add, LieIdeal.derivedSeries_add_eq_bot, add_eq_sup, LieAlgebra.isSolvableAdd
|
instAddCommMonoid π | CompOp | β |
instBot π | CompOp | 93 mathmath: LieModule.trivial_iff_lower_central_eq_bot, LieAlgebra.derivedLength_zero, bot_toSubmodule, LieModule.traceForm_eq_sum_genWeightSpaceOf, LieAlgebra.isSolvable_iff_int, LieModuleHom.ker_eq_bot, bot_lie, lie_abelian_iff_lie_self_eq_bot, LieAlgebra.hasTrivialRadical_iff, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, isNilpotent_iff_exists_lcs_eq_bot, LieModule.nilpotencyLength_eq_succ_iff, LieModuleHom.ker_id, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieModule.iSup_ucs_le_genWeightSpace_zero, lie_bot, lowerCentralSeries_eq_bot_iff_lcs_eq_bot, LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff, subsingleton_of_bot, bot_coe, isNilpotent_iff_exists_self_le_ucs, comap_incl_eq_bot, LieHom.ker_eq_bot, ucs_comap_incl, LieModule.isNilpotent_iff, lieSpan_eq_bot_iff, LieModule.isNilpotent_iff_int, LieModule.IsNilpotent.nilpotent, LieModule.finite_genWeightSpaceOf_ne_bot, LieIdeal.subsingleton_of_bot, LieAlgebra.isSolvable_iff, trivial_lie_oper_zero, LieModule.posFittingCompOf_eq_bot_of_isNilpotent, LieAlgebra.abelian_iff_derived_one_eq_bot, LieModuleHom.le_ker_iff_map, LieModule.existsβ_genWeightSpace_smul_add_eq_bot, LieModule.genWeightSpace_chainBotCoeff_sub_one_zsmul_sub, ker_incl, mem_bot, LieAlgebra.IsKilling.rootSpace_one_div_two_smul, LieAlgebra.hasTrivialRadical_iff_no_solvable_ideals, LieAlgebra.IsExtension.ker_eq_bot, LieAlgebra.IsSolvable.solvable_int, LieModule.ideal_oper_maxTrivSubmodule_eq_bot, LieModule.genWeightSpace_chainTopCoeff_add_one_zsmul_add, Quotient.map_mk'_eq_bot_le, LieModule.isNilpotent_iff_exists_ucs_eq_top, LieModule.exists_genWeightSpace_smul_add_eq_bot, LieModule.finite_genWeightSpace_ne_bot, LieIdeal.derivedSeries_eq_bot_iff, LieAlgebra.center_eq_bot, LieModule.isFaithful_iff_ker_eq_bot, LieModule.chainTopCoeff_add_one, LieModule.le_max_triv_iff_bracket_eq_bot, LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian, ucs_le_of_normalizer_eq_self, LieModule.eventually_genWeightSpace_smul_add_eq_bot, LieAlgebra.HasTrivialRadical.radical_eq_bot, LieSubalgebra.normalizer_eq_self_iff, mk_eq_bot_iff, LieAlgebra.IsKilling.killingCompl_top_eq_bot, LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals, LieAlgebra.isFaithful_self_iff, LieModule.iSup_ucs_eq_genWeightSpace_zero, LieModule.IsNilpotent.nilpotent_int, LieAlgebra.derivedSeries_of_bot_eq_bot, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_bot_iff, LieAlgebra.abelian_iff_derived_succ_eq_bot, map_bot, LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, LieAlgebra.IsKilling.rootSpace_two_smul, LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable, LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical, LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent, toSubmodule_eq_bot, LieAlgebra.isSolvableBot, LieModule.injOn_genWeightSpace, LieAlgebra.IsSolvable.solvable, LieModule.posFittingComp_eq_bot_of_isNilpotent, ucs_bot_one, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, span_empty, lie_eq_bot_iff, LieModule.genWeightSpace_neg_add_chainBot, eq_bot_iff, LieIdeal.ker_incl, normalizer_bot_eq_maxTrivSubmodule, LieModule.genWeightSpace_add_chainTop, LieIdeal.comap_incl_eq_bot, LieIdeal.map_eq_bot_iff, LieAlgebra.IsSimple.eq_bot_or_eq_top, LieModule.ker_eq_bot, baseChange_bot
|
instCompleteLattice π | CompOp | 23 mathmath: LieModule.disjoint_genWeightSpaceOf, LieAlgebra.IsSemisimple.booleanGenerators, disjoint_toSubmodule, isCompl_toSubmodule, LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, LieAlgebra.IsSimple.isAtom_top, instIsCompactlyGenerated, LieIdeal.isCompl_killingCompl, LieModule.isCompl_genWeightSpace_zero_posFittingComp, instIsAtomicOfIsArtinian, LieModule.iSupIndep_genWeightSpace, codisjoint_toSubmodule, LieModule.iSupIndep_genWeightSpaceOf, LieAlgebra.InvariantForm.atomistic, LieModule.iSupIndep_genWeightSpace', LieAlgebra.IsSemisimple.sSupIndep_isAtom, iSupIndep_toSubmodule, LieAlgebra.IsSimple.isAtom_iff_eq_top, instIsModularLattice, LieIdeal.comap_incl_eq_bot, LieModule.disjoint_genWeightSpace, LieModule.isCompl_genWeightSpaceOf_zero_posFittingCompOf
|
instInfSet π | CompOp | 13 mathmath: LieModule.iInf_lowerCentralSeries_eq_posFittingComp, LieModule.posFittingComp_le_iInf_lowerCentralSeries, mem_iInf, sInf_toSubmodule, iInf_coe, iInf_toSubmodule, LieModule.iInf_lcs_le_of_isNilpotent_quot, sInf_toSubmodule_eq_iInf, coe_sInf, LieModule.eventually_iInf_lowerCentralSeries_eq, LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent, coe_iInf, sInf_coe
|
instInhabited π | CompOp | β |
instLieRingModuleSubtypeMem π | CompOp | 80 mathmath: LieAlgebra.abelian_radical_of_hasTrivialRadical, TensorProduct.LieModule.mapIncl_def, LieModule.traceForm_eq_sum_genWeightSpaceOf, lie_abelian_iff_lie_self_eq_bot, LieModule.isNilpotent_toEnd_genWeightSpace_zero, isNilpotent_iff_exists_lcs_eq_bot, LieModule.trace_toEnd_genWeightSpace, LieModule.trivial_iff_le_maximal_trivial, LieModule.shiftedGenWeightSpace.toEnd_eq, LieModule.instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule, LieModule.instIsTriangularizableSubtypeMemLieSubmodule_1, LieAlgebra.derivedSeries_of_derivedLength_succ, traceForm_eq_of_le_idealizer, incl_apply, LieAlgebra.Extension.toKer_bracket, lowerCentralSeries_eq_bot_iff_lcs_eq_bot, lowerCentralSeries_map_eq_lcs, LieAlgebra.abelian_radical_iff_solvable_is_abelian, map_incl_top, subsingleton_of_bot, isNilpotent_iff_exists_self_le_ucs, comap_incl_eq_top, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, comap_incl_eq_bot, ucs_comap_incl, range_incl, map_incl_lt_iff_lt_top, LieAlgebra.Extension.ringModuleOf_bracket, LieIdeal.isLieAbelian_iff, LieAlgebra.abelian_iff_derived_one_eq_bot, ker_incl, toEnd_restrict_eq_toEnd, LieModuleHom.codRestrict_apply, LieModule.trace_comp_toEnd_genWeightSpace_eq, LieModule.instMaxNilpotentSubmoduleIsNilpotent, coe_inclusion, LieModuleHom.comp_ker_incl, map_incl_le, LieModule.maxTrivEquiv_of_equiv_symm_eq_symm, lowerCentralSeries_eq_lcs_comap, LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal, LieModule.isNilpotent_of_top_iff', coe_toEnd, coe_bracket, LieAlgebra.IsSemisimple.non_abelian_of_isAtom, LieAlgebra.abelian_of_le_center, LieModuleEquiv.ofTop_apply, LieModule.isNilpotent_toEnd_sub_algebraMap, incl_eq_val, LieModule.maxTrivEquiv_of_refl_eq_refl, inclusion_apply, LieModule.isNilpotent_iff_le_maxNilpotentSubmodule, LieModule.traceForm_genWeightSpace_eq, LieModule.instIsNilpotentSup, LieModule.instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, lieIdeal_oper_eq_tensor_map_range, LieIdeal.isLieAbelian_of_trivial, LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq, LieAlgebra.Extension.ringModuleOf_bracket_proj, LieAlgebra.abelian_derivedAbelianOfIdeal, LieAlgebra.abelian_iff_derived_succ_eq_bot, coe_toEnd_pow, LieModule.coe_maxTrivEquiv_apply, LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter, instIsLieTowerSubtypeMemLieSubmodule_1, inclusion_injective, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, incl_coe, LieAlgebra.maxNilpotentIdealIsNilpotent, LieModule.coe_maxTrivHom_apply, instLieModule, injective_incl, map_comap_incl, LieModule.isNilpotent_of_le, comap_incl_self, LieAlgebra.rootSpaceProduct_tmul, LieModule.posFittingComp_map_incl_sup_of_codisjoint, LieModule.coe_lowerCentralSeries_ideal_le, LieModule.genWeightSpace_genWeightSpaceOf_map_incl
|
instMax π | CompOp | 17 mathmath: lie_sup, lcs_sup, sup_lie, span_union, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, sup_toSubmodule, LieIdeal.map_sup_ker_eq_map', mem_sup, LieIdeal.comap_map_eq, map_sup, LieModule.instIsNilpotentSup, add_eq_sup, LieIdeal.comap_bracket_eq, LieIdeal.map_sup_ker_eq_map, LieModule.posFittingComp_map_incl_sup_of_codisjoint, LieIdeal.map_sup
|
instMin π | CompOp | 20 mathmath: LieIdeal.map_comap_incl, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, map_inf_le, mem_inf, lie_inf, comap_incl_eq_bot, lie_le_inf, LieModule.map_genWeightSpace_eq_of_injective, map_inf, coe_inf, normalizer_inf, LieIdeal.comap_bracket_incl, LieIdeal.map_comap_bracket_eq, inf_lie, LieIdeal.map_comap_eq, comap_inf, map_comap_incl, LieIdeal.comap_bracket_eq, inf_toSubmodule, inf_coe
|
instPartialOrder π | CompOp | 104 mathmath: LieIdeal.map_bracket_le, LieIdeal.comap_incl_eq_top, toSubmodule_le_toSubmodule, LieModule.posFittingComp_le_iInf_lowerCentralSeries, isCompactElement_lieSpan_singleton, LieModule.derivedSeries_le_lowerCentralSeries, LieIdeal.gc_map_comap, lcs_add_le_iff, LieModule.disjoint_genWeightSpaceOf, LieAlgebra.IsSemisimple.booleanGenerators, lie_le_iff, LieAlgebra.derivedSeriesOfIdeal_succ_le, map_inf_le, LieModule.map_genWeightSpace_le, LieModule.trivial_iff_le_maximal_trivial, disjoint_toSubmodule, LieModule.iSup_ucs_le_genWeightSpace_zero, isCompl_toSubmodule, toSubmodule_orderEmbedding_apply, orderIsoMapComap_apply, lie_inf, isNilpotent_iff_exists_self_le_ucs, LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff, comap_incl_eq_top, LieIdeal.le_killingCompl_top_of_isLieAbelian, LieIdeal.derivedSeries_map_le, map_incl_lt_iff_lt_top, LieModule.genWeightSpace_le_genWeightSpaceOf, lie_le_inf, LieAlgebra.derivedSeriesOfIdeal_le_self, monotone_normalizer, orderIsoMapComap_symm_apply, LieModule.lowerCentralSeriesLast_le_of_not_isTrivial, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, LieAlgebra.IsSimple.isAtom_top, LieIdeal.isLieAbelian_iff, LieIdeal.map_mono, LieModuleHom.le_ker_iff_map, LieModule.antitone_lowerCentralSeries, LieAlgebra.center_le_radical, LieModule.iInf_lcs_le_of_isNilpotent_quot, LieHom.ker_le_comap, LieIdeal.comap_bracket_le, LieIdeal.map_lowerCentralSeries_le, map_comap_le, LieAlgebra.derivedSeriesOfIdeal_antitone, ucs_eq_top_iff, top_lie_le_iff_le_normalizer, LieModule.lowerCentralSeriesLast_le_max_triv, LieAlgebra.derivedSeriesOfIdeal_add_le_add, map_incl_le, LieModule.isNilpotent_quotient_iff, LieModule.genWeightSpace_le_genWeightSpaceChain, Quotient.map_mk'_eq_bot_le, LieIdeal.isCompl_killingCompl, lieSpan_mono, wellFoundedLT_of_isArtinian, LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal, LieModule.isCompl_genWeightSpace_zero_posFittingComp, lcs_le_iff, instIsAtomicOfIsArtinian, LieModule.le_max_triv_iff_bracket_eq_bot, LieIdeal.comap_mono, wellFoundedGT_of_noetherian, ucs_le_of_normalizer_eq_self, inf_lie, lie_le_right, gc_map_comap, LieModule.weightSpace_le_genWeightSpace, LieModule.map_lowerCentralSeries_le, LieIdeal.comap_map_le, LieModule.isNilpotent_iff_le_maxNilpotentSubmodule, LieIdeal.map_le_iff_le_comap, codisjoint_toSubmodule, le_normalizer, LieAlgebra.derivedSeries_lt_top_of_solvable, LieModule.posFittingCompOf_le_lowerCentralSeries, mapOrderEmbedding_apply, LieHom.map_le_idealRange, lieSpan_le, LieIdeal.map_le, LieAlgebra.toLieSubmodule_le_rootSpace_zero, map_le_map_iff, LieAlgebra.center_le_maxNilpotentIdeal, LieModule.posFittingCompOf_le_posFittingComp, map_le_iff_le_comap, LieAlgebra.maxNilpotentIdeal_le_radical, gc_lcs_ucs, LieAlgebra.InvariantForm.atomistic, map_le_range, LieModule.map_posFittingComp_le, lcs_le_self, LieHom.le_ker_iff, LieAlgebra.IsSemisimple.sSupIndep_isAtom, le_comap_map, LieAlgebra.LieIdeal.solvable_iff_le_radical, LieAlgebra.IsSimple.isAtom_iff_eq_top, lie_le_left, LieIdeal.comap_incl_eq_bot, LieIdeal.map_eq_bot_iff, LieIdeal.map_comap_le, gc_top_lie_normalizer, LieModule.disjoint_genWeightSpace, LieModule.isCompl_genWeightSpaceOf_zero_posFittingCompOf
|
instSetLike π | CompOp | 232 mathmath: LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map, coe_smul, LieModule.shiftedGenWeightSpace.shift_apply, LieAlgebra.Extension.incl_apply_mem_ker, LieModuleHom.mem_range, coe_map, LieAlgebra.abelian_radical_of_hasTrivialRadical, LieAlgebra.IsSemisimple.isSimple_of_isAtom, LieIdeal.comap_incl_eq_top, LieModule.Weight.exists_ne_zero, TensorProduct.LieModule.mapIncl_def, Quotient.mk_eq_zero, LieIdeal.restrict_killingForm, coe_toSet_mk, mem_comap, LieIdeal.coe_bracket_of_module, LieModule.traceForm_eq_sum_genWeightSpaceOf, LieModule.traceForm_eq_sum_finrank_nsmul', LieAlgebra.InvariantForm.orthogonal_carrier, LieHom.mem_idealRange, lie_abelian_iff_lie_self_eq_bot, LieModule.shiftedGenWeightSpace.instSubtypeMemLieSubmodule, LieIdeal.map_comap_incl, coe_sub, LieModule.isNilpotent_toEnd_genWeightSpace_zero, isNilpotent_iff_exists_lcs_eq_bot, LieIdeal.incl_injective, LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap, lie_le_iff, LieModule.exists_nontrivial_weightSpace_of_lieIdeal, LieAlgebra.le_solvable_ideal_solvable, LieModule.trace_toEnd_genWeightSpace, mem_inf, LieModule.trivial_iff_le_maximal_trivial, lieIdeal_oper_eq_linear_span', LieModule.shiftedGenWeightSpace.toEnd_eq, mem_mk_iff', LieModule.instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, mem_toSubmodule, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom, LieModule.instIsTriangularizableSubtypeMemLieSubmodule_1, RootPairing.GeckConstruction.mem_ΟConjLieSubmodule_iff, LieAlgebra.derivedSeries_of_derivedLength_succ, traceForm_eq_of_le_idealizer, LieModule.mem_weightSpace, incl_apply, LieModule.mem_posFittingCompOf, LieAlgebra.Extension.toKer_bracket, LieAlgebra.non_trivial_center_of_isNilpotent, LieIdeal.instIsNilpotentSubtypeMemLieSubmoduleOfIsNilpotent, mem_iInf, coe_zero, LieIdeal.comap_bracket_incl_of_le, lowerCentralSeries_eq_bot_iff_lcs_eq_bot, LieModuleHom.mem_ker, LieIdeal.coe_toLieSubalgebra, instSMulMemClass, lowerCentralSeries_map_eq_lcs, LieIdeal.mem_killingCompl, LieAlgebra.abelian_radical_iff_solvable_is_abelian, LieModule.instIsTriangularizableSubtypeMemLieSubmodule, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, map_incl_top, subsingleton_of_bot, bot_coe, iInf_coe, LieModule.mem_genWeightSpace, isNilpotent_iff_exists_self_le_ucs, LieModule.mem_ker, comap_incl_eq_top, LieIdeal.incl_coe, LieAlgebra.Extension.lie_incl_mem_ker, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, comap_incl_eq_bot, ucs_comap_incl, LieModule.nontrivial_max_triv_of_isNilpotent, instIsTorsionFreeSubtypeMem, range_incl, LieIdeal.incl_isIdealMorphism, map_incl_lt_iff_lt_top, LieIdeal.lieModule, LieIdeal.subsingleton_of_bot, LieSubalgebra.mem_toLieSubmodule, LinearMap.BilinForm.lieInvariant_iff, subset_lieSpan, LieAlgebra.Extension.ringModuleOf_bracket, mem_baseChange_iff, LieIdeal.isLieAbelian_iff, mem_mk_iff, mapsTo_pow_toEnd_sub_algebraMap, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieAlgebra.abelian_iff_derived_one_eq_bot, LieIdeal.incl_range, LieModule.exists_nontrivial_weightSpace_of_isNilpotent, LieModule.mem_maxTrivSubmodule, ker_incl, instIsArtinianSubtypeMem, toEnd_restrict_eq_toEnd, LieIdeal.coe_inclusion, mem_bot, LieIdeal.inclusion_injective, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, LieModuleHom.coe_range, LieModule.trace_comp_toEnd_genWeightSpace_eq, zero_mem, LieModule.instMaxNilpotentSubmoduleIsNilpotent, coe_inclusion, LieModule.iterate_toEnd_mem_lowerCentralSeriesβ, LieModuleHom.comp_ker_incl, LieIdeal.topEquiv_apply, LieModule.mem_posFittingComp, map_incl_le, coe_inf, LieModule.maxTrivEquiv_of_equiv_symm_eq_symm, LieModule.shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply, lowerCentralSeries_eq_lcs_comap, lieSpan_eq, LieModule.traceForm_eq_sum_finrank_nsmul, LieDerivation.IsKilling.rangeAdOrthogonal_carrier, mem_sup, LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal, LieIdeal.derivedSeries_eq_bot_iff, sSup_image_lieSpan_singleton, LieIdeal.comap_bracket_incl, LieModule.shiftedGenWeightSpace.instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian, mem_idealizer, LieIdeal.killingForm_eq, LieModule.isNilpotent_of_top_iff', ext_iff, coe_toEnd, LieAlgebra.InvariantForm.mem_orthogonal, coe_neg, LieIdeal.coe_derivedSeries_eq_int, LieModule.exists_nontrivial_weightSpace_of_isSolvable, coe_bracket, LieAlgebra.IsSemisimple.non_abelian_of_isAtom, LieAlgebra.abelian_of_le_center, LieModuleEquiv.ofTop_apply, LieModule.isNilpotent_toEnd_sub_algebraMap, LieIdeal.incl_idealRange, coe_injective, LieIdeal.comap_incl_self, incl_eq_val, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieModule.maxTrivEquiv_of_refl_eq_refl, Quotient.mk_eq_zero', LieHom.mem_ker, nontrivial_iff_ne_bot, LieModule.coe_lowerCentralSeries_eq_int, inclusion_apply, coe_toSubmodule, top_coe, LieHom.range_subset_idealRange, LieAlgebra.radicalIsSolvable, LieModule.isNilpotent_iff_le_maxNilpotentSubmodule, LieModule.traceForm_genWeightSpace_eq, LieModule.instIsNilpotentSup, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, LieIdeal.mem_comap, LieModule.instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian, LieModule.zero_lt_finrank_genWeightSpace, lieIdeal_oper_eq_tensor_map_range, LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm, LieIdeal.isLieAbelian_of_trivial, coe_sInf, lieIdeal_oper_eq_linear_span, LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq, LieAlgebra.mem_corootSpace', mem_top, LieAlgebra.Extension.ringModuleOf_bracket_proj, LieAlgebra.abelian_derivedAbelianOfIdeal, LieModule.nontrivial_lowerCentralSeriesLast, lieIdeal_oper_eq_span, LieAlgebra.abelian_iff_derived_succ_eq_bot, coe_toEnd_pow, lieSpan_le, LieModule.mem_genWeightSpaceOf, LieIdeal.map_le, LieModule.traceForm_eq_sum_finrank_nsmul_mul, LieModule.coe_maxTrivEquiv_apply, LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter, instIsLieTowerSubtypeMemLieSubmodule_1, instIsNoetherianSubtypeMem, mem_carrier, inclusion_injective, exists_smul_add_of_span_sup_eq_top, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, LieHom.mem_idealRange_iff, incl_coe, LieAlgebra.mem_corootSpace, LieModule.iterate_toEnd_mem_lowerCentralSeries, LieAlgebra.isSolvableAdd, LieAlgebra.maxNilpotentIdealIsNilpotent, LieModule.coe_maxTrivHom_apply, LieIdeal.coe_lcs_eq, mem_lieSpan, instAddSubgroupClass, instLieModule, LieDerivation.mem_ad_idealRange_iff, LieAlgebra.derivedLength_eq_derivedLengthOfIdeal, instIsLieTowerSubtypeMemLieSubmodule, LieAlgebra.Extension.twoCocycleOf_coe_coe, injective_incl, LieAlgebra.isSolvableBot, map_comap_incl, LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, LieModule.shiftedGenWeightSpace.shift_symm_apply, LieAlgebra.LieIdeal.solvable_iff_le_radical, LieIdeal.incl_apply, Function.instIsSolvableSubtypeMemLieSubmodule, coe_iInf, mem_normalizer, LieModule.isNilpotent_of_le, LieAlgebra.Extension.lie_toKer_apply, comap_incl_self, LieAlgebra.rootSpaceProduct_tmul, LieModule.posFittingComp_map_incl_sup_of_codisjoint, coe_add, LieIdeal.ker_incl, LieModule.coe_maxTrivLinearMapEquivLieModuleHom, LieIdeal.comap_incl_eq_bot, LieIdeal.inclusion_apply, mem_map, lie_coe_mem_lie, LieModule.coe_lowerCentralSeries_ideal_le, LieAlgebra.Extension.oneCochainOfTwoSplitting_apply, sInf_coe, LieAlgebra.isExtension_of_surjective, LieModule.genWeightSpace_genWeightSpaceOf_map_incl, mem_coe, inf_coe
|
instSupSet π | CompOp | 22 mathmath: map_iSup, iSup_toSubmodule, LieModule.iSup_genWeightSpaceOf_eq_top, LieModule.genWeightSpaceChain_def', LieModule.iSup_genWeightSpace_eq_top', LieModule.iSup_ucs_le_genWeightSpace_zero, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, span_iUnion, LieModule.mem_posFittingComp, mem_iSup_of_mem, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, sSup_toSubmodule, sSup_image_lieSpan_singleton, LieModule.genWeightSpaceChain_def, sSup_toSubmodule_eq_iSup, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieModule.iSup_genWeightSpace_eq_top, LieModule.iSup_ucs_eq_genWeightSpace_zero, iSup_toSubmodule_eq_top, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.InvariantForm.atomistic
|
instTop π | CompOp | 63 mathmath: LieIdeal.comap_incl_eq_top, LieModule.lowerCentralSeries_zero, LieModule.iSup_genWeightSpaceOf_eq_top, LieModule.iSup_genWeightSpace_eq_top', LieIdeal.coe_killingCompl_top, lie_top_eq_of_span_sup_eq_top, map_incl_top, span_univ, mk_eq_top_iff, comap_incl_eq_top, LieIdeal.le_killingCompl_top_of_isLieAbelian, LieAlgebra.radical_eq_top_of_isSolvable, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, LieAlgebra.IsSimple.eq_top_of_isAtom, map_incl_lt_iff_lt_top, LieModule.lowerCentralSeries_succ, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, Quotient.range_mk', top_toSubmodule, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, LieAlgebra.IsSimple.isAtom_top, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, ucs_eq_top_iff, top_lie_le_iff_le_normalizer, LieIdeal.topEquiv_apply, LieModule.maxNilpotentSubmodule_eq_top_of_isNilpotent, RootPairing.GeckConstruction.ΟConjLieSubmodule_eq_top_iff, LieAlgebra.derivedSeries_def, eq_top_of_isIrreducible, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_top_iff, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieModuleHom.range_eq_top, LieModule.isNilpotent_iff_exists_ucs_eq_top, LieModule.isNilpotent_of_top_iff', LieAlgebra.isLieAbelian_iff_center_eq_top, LieHom.idealRange_eq_map, LieModule.le_max_triv_iff_bracket_eq_bot, LieAlgebra.maxNilpotentIdeal_eq_top_of_isNilpotent, LieModuleEquiv.ofTop_apply, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, LieIdeal.comap_incl_self, LieModule.iSup_genWeightSpace_eq_top, LieAlgebra.IsKilling.killingCompl_top_eq_bot, top_coe, LieIdeal.lcs_zero, LieModule.isTrivial_iff_max_triv_eq_top, LieModule.zero_genWeightSpace_eq_top_of_nilpotent', LieIdeal.top_toLieSubalgebra, iSup_toSubmodule_eq_top, LieAlgebra.derivedSeries_lt_top_of_solvable, mem_top, LieIdeal.derivedSeries_succ_eq_top_iff, lcs_succ, toSubmodule_eq_top, baseChange_top, LieAlgebra.IsSimple.isAtom_iff_eq_top, LieModuleHom.map_top, comap_incl_self, LieIdeal.lcs_top, LieModuleEquiv.range_coe, LieAlgebra.IsSimple.eq_bot_or_eq_top, LieHom.idealRange_eq_top_of_surjective, gc_top_lie_normalizer
|
instUniqueBot π | CompOp | β |
instUniqueOfSubsingleton π | CompOp | β |
instZero π | CompOp | β |
lieSpan π | CompOp | 16 mathmath: isCompactElement_lieSpan_singleton, span_univ, lieSpan_eq_bot_iff, span_union, subset_lieSpan, span_iUnion, lieSpan_mono, lieSpan_eq, sSup_image_lieSpan_singleton, coe_lieSpan_submodule_eq_iff, LieHom.idealRange_eq_lieSpan_range, lieIdeal_oper_eq_span, lieSpan_le, mem_lieSpan, submodule_span_le_lieSpan, span_empty
|
map π | CompOp | 41 mathmath: map_iSup, coe_map, map_injective_of_injective, map_inf_le, LieModule.map_genWeightSpace_le, orderIsoMapComap_apply, lowerCentralSeries_map_eq_lcs, map_incl_top, toSubmodule_map, map_incl_lt_iff_lt_top, LieModule.map_genWeightSpace_eq_of_injective, LieModule.map_genWeightSpace_eq, LieModuleHom.le_ker_iff_map, map_inf, map_comap_le, comap_map_eq, map_incl_le, Quotient.map_mk'_eq_bot_le, LieModule.map_posFittingComp_eq, map_id, gc_map_comap, LieModule.map_lowerCentralSeries_le, map_sup, mapOrderEmbedding_apply, map_bot, mem_map_of_mem, LieModule.map_lowerCentralSeries_eq, map_comp, map_le_map_iff, map_le_iff_le_comap, map_comap_eq, map_le_range, LieModule.map_posFittingComp_le, map_bracket_eq, le_comap_map, map_comap_incl, LieModuleHom.map_top, map_mono, LieModule.posFittingComp_map_incl_sup_of_codisjoint, mem_map, LieModule.genWeightSpace_genWeightSpaceOf_map_incl
|
mapOrderEmbedding π | CompOp | 1 mathmath: mapOrderEmbedding_apply
|
orderIsoMapComap π | CompOp | 2 mathmath: orderIsoMapComap_apply, orderIsoMapComap_symm_apply
|
toSubmodule π | CompOp | 68 mathmath: Submodule.exists_lieSubmodule_coe_eq_iff, instCanLiftSubmoduleToSubmoduleForallForallForallMemBracket, bot_toSubmodule, toSubmodule_le_toSubmodule, iSup_toSubmodule, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, LieAlgebra.coe_zeroRootSubalgebra, lieIdeal_oper_eq_linear_span', mem_toSubmodule, disjoint_toSubmodule, toSubmodule_injective, isCompl_toSubmodule, toSubmodule_orderEmbedding_apply, lie_top_eq_of_span_sup_eq_top, sInf_toSubmodule, LieModuleHom.toSubmodule_range, coe_map_toEnd_le, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', toSubmodule_map, LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, LieModule.coe_genWeightSpaceOf_zero, LieSubalgebra.coe_normalizer_eq_normalizer, LieIdeal.toLieSubalgebra_toSubmodule, LieIdeal.map_toSubmodule, trace_eq_trace_restrict_of_le_idealizer, top_toSubmodule, mem_baseChange_iff, iInf_toSubmodule, toSubmodule_inj, toEnd_restrict_eq_toEnd, coe_lowerCentralSeries_ideal_quot_eq, Function.Surjective.lieModule_lcs_map_eq, sup_toSubmodule, LieIdeal.coe_map_of_surjective, LieModuleHom.ker_toSubmodule, sSup_toSubmodule, LieModule.coe_genWeightSpace_of_top, sInf_toSubmodule_eq_iInf, coe_lieSpan_submodule_eq_iff, LieSubalgebra.coe_toLieSubmodule, LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule, sSup_toSubmodule_eq_iSup, toSubmodule_comap, coe_toSubmodule, codisjoint_toSubmodule, iSup_toSubmodule_eq_top, lieIdeal_oper_eq_linear_span, LieAlgebra.InvariantForm.orthogonal_toSubmodule, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, mem_carrier, LieModule.coe_lcs_range_toEnd_eq, incl_coe, LieIdeal.toSubmodule_killingCompl, toSubmodule_eq_top, LieHom.ker_toSubmodule, LieIdeal.coe_lcs_eq, toSubmodule_eq_bot, coe_baseChange, submodule_span_le_lieSpan, iSupIndep_toSubmodule, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, toSubmodule_mk, lieModule_lcs_map_le, LieModule.coe_lowerCentralSeries_ideal_le, LieIdeal.comap_toSubmodule, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, inf_toSubmodule, Quotient.is_quotient_mk
|
toSubmodule_orderEmbedding π | CompOp | 1 mathmath: toSubmodule_orderEmbedding_apply
|
| Name | Category | Theorems |
|---|
LieSubmodule π | CompData | 395 mathmath: LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map, LieSubmodule.coe_smul, LieModule.shiftedGenWeightSpace.shift_apply, LieSubmodule.map_iSup, LieModule.trivial_iff_lower_central_eq_bot, LieModuleHom.mem_range, LieModule.iInf_lowerCentralSeries_eq_posFittingComp, LieSubmodule.coe_map, LieSubmodule.instCanLiftSubmoduleToSubmoduleForallForallForallMemBracket, LieAlgebra.abelian_radical_of_hasTrivialRadical, LieAlgebra.IsSemisimple.isSimple_of_isAtom, LieSubmodule.lie_sup, LieIdeal.comap_incl_eq_top, LieModule.Weight.exists_ne_zero, TensorProduct.LieModule.mapIncl_def, LieSubmodule.map_injective_of_injective, LieModule.lowerCentralSeries_zero, LieSubmodule.Quotient.mk_eq_zero, LieSubmodule.bot_toSubmodule, LieIdeal.restrict_killingForm, LieSubmodule.coe_toSet_mk, LieSubmodule.toSubmodule_le_toSubmodule, LieSubmodule.iSup_toSubmodule, LieSubmodule.mem_comap, LieIdeal.coe_bracket_of_module, LieModule.traceForm_eq_sum_genWeightSpaceOf, LieModule.posFittingComp_le_iInf_lowerCentralSeries, LieSubmodule.lcs_sup, LieModule.traceForm_eq_sum_finrank_nsmul', LieAlgebra.InvariantForm.orthogonal_carrier, LieSubmodule.isCompactElement_lieSpan_singleton, LieModuleHom.ker_eq_bot, LieModule.iSup_genWeightSpaceOf_eq_top, LieSubmodule.bot_lie, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieModule.shiftedGenWeightSpace.instSubtypeMemLieSubmodule, LieSubmodule.lcs_add_le_iff, LieIdeal.map_comap_incl, LieModule.disjoint_genWeightSpaceOf, LieSubmodule.coe_sub, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, LieModule.isNilpotent_toEnd_genWeightSpace_zero, LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot, LieIdeal.incl_injective, LieModule.nilpotencyLength_eq_succ_iff, LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap, LieModule.genWeightSpaceChain_def', LieSubmodule.lie_le_iff, LieModule.exists_nontrivial_weightSpace_of_lieIdeal, LieModuleHom.ker_id, LieAlgebra.le_solvable_ideal_solvable, LieModule.trace_toEnd_genWeightSpace, LieSubmodule.map_inf_le, LieSubmodule.mem_inf, LieModule.map_genWeightSpace_le, LieModule.trivial_iff_le_maximal_trivial, LieSubmodule.Quotient.mk'_ker, LieSubmodule.lieIdeal_oper_eq_linear_span', LieModule.shiftedGenWeightSpace.toEnd_eq, LieModule.iSup_genWeightSpace_eq_top', LieSubmodule.mem_mk_iff', LieModule.instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule, LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieSubmodule.mem_toSubmodule, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom, LieSubmodule.disjoint_toSubmodule, LieModule.instIsTriangularizableSubtypeMemLieSubmodule_1, LieSubmodule.toSubmodule_injective, RootPairing.GeckConstruction.mem_ΟConjLieSubmodule_iff, LieSubmodule.Quotient.toEnd_comp_mk', LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieModule.iSup_ucs_le_genWeightSpace_zero, LieAlgebra.derivedSeries_of_derivedLength_succ, LieSubmodule.traceForm_eq_of_le_idealizer, LieModule.mem_weightSpace, LieSubmodule.incl_apply, LieModule.mem_posFittingCompOf, LieSubmodule.lie_bot, LieSubmodule.isCompl_toSubmodule, LieAlgebra.Extension.toKer_bracket, LieAlgebra.non_trivial_center_of_isNilpotent, LieIdeal.instIsNilpotentSubtypeMemLieSubmoduleOfIsNilpotent, LieSubmodule.mem_iInf, LieSubmodule.toSubmodule_orderEmbedding_apply, LieSubmodule.coe_zero, LieIdeal.comap_bracket_incl_of_le, LieSubmodule.lowerCentralSeries_eq_bot_iff_lcs_eq_bot, LieModuleHom.mem_ker, LieSubmodule.orderIsoMapComap_apply, LieSubmodule.lie_top_eq_of_span_sup_eq_top, LieSubmodule.lie_inf, LieSubmodule.sInf_toSubmodule, LieSubmodule.instSMulMemClass, LieSubmodule.lowerCentralSeries_map_eq_lcs, LieAlgebra.abelian_radical_iff_solvable_is_abelian, LieModule.instIsTriangularizableSubtypeMemLieSubmodule, LieSubmodule.sup_lie, LieSubmodule.map_incl_top, LieSubmodule.subsingleton_of_bot, LieSubmodule.bot_coe, LieSubmodule.iInf_coe, LieModule.mem_genWeightSpace, LieSubmodule.span_univ, LieSubmodule.isNilpotent_iff_exists_self_le_ucs, LieSubmodule.mk_eq_top_iff, LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff, LieSubmodule.comap_incl_eq_top, LieIdeal.incl_coe, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieSubmodule.comap_incl_eq_bot, LieSubmodule.ucs_comap_incl, LieModule.nontrivial_max_triv_of_isNilpotent, LieModule.isNilpotent_iff, LieSubmodule.instIsTorsionFreeSubtypeMem, LieSubmodule.range_incl, LieIdeal.incl_isIdealMorphism, LieSubmodule.lieSpan_eq_bot_iff, LieSubmodule.map_incl_lt_iff_lt_top, LieModule.isNilpotent_iff_int, LieSubmodule.span_union, LieModule.genWeightSpace_le_genWeightSpaceOf, LieModule.IsNilpotent.nilpotent, LieModule.lowerCentralSeries_succ, LieModule.finite_genWeightSpaceOf_ne_bot, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, LieIdeal.lieModule, LieSubmodule.monotone_normalizer, LieModule.map_genWeightSpace_eq_of_injective, LieSubmodule.orderIsoMapComap_symm_apply, LieIdeal.subsingleton_of_bot, LieSubalgebra.mem_toLieSubmodule, LieModule.lowerCentralSeriesLast_le_of_not_isTrivial, LinearMap.BilinForm.lieInvariant_iff, LieSubmodule.Quotient.range_mk', LieSubmodule.trace_eq_trace_restrict_of_le_idealizer, LieSubmodule.subset_lieSpan, LieAlgebra.Extension.ringModuleOf_bracket, LieSubmodule.top_toSubmodule, LieSubmodule.mem_baseChange_iff, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, LieSubmodule.iInf_toSubmodule, LieIdeal.lcs_succ, LieIdeal.isLieAbelian_iff, LieSubmodule.span_iUnion, LieSubmodule.mem_mk_iff, LieSubmodule.trivial_lie_oper_zero, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, LieSubmodule.mono_lie_left, LieIdeal.mem_map_of_surjective, LieModule.posFittingCompOf_eq_bot_of_isNilpotent, LieAlgebra.abelian_iff_derived_one_eq_bot, LieIdeal.incl_range, LieModule.exists_nontrivial_weightSpace_of_isNilpotent, LieModuleHom.le_ker_iff_map, LieModule.mem_maxTrivSubmodule, LieModule.existsβ_genWeightSpace_smul_add_eq_bot, LieModule.genWeightSpace_chainBotCoeff_sub_one_zsmul_sub, LieSubmodule.instIsCompactlyGenerated, LieSubmodule.ker_incl, LieSubmodule.map_inf, LieModule.antitone_lowerCentralSeries, LieSubmodule.instIsArtinianSubtypeMem, LieModule.iInf_lcs_le_of_isNilpotent_quot, LieSubmodule.toEnd_restrict_eq_toEnd, LieIdeal.coe_inclusion, LieSubmodule.mem_bot, LieIdeal.inclusion_injective, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, LieAlgebra.IsKilling.rootSpace_one_div_two_smul, LieModuleHom.coe_range, LieModule.trace_comp_toEnd_genWeightSpace_eq, LieSubmodule.zero_mem, LieModule.instMaxNilpotentSubmoduleIsNilpotent, LieSubmodule.sup_toSubmodule, LieSubmodule.map_comap_le, LieModule.iterate_toEnd_mem_lowerCentralSeriesβ, LieModuleHom.comp_ker_incl, LieSubmodule.lie_baseChange, LieSubmodule.ucs_eq_top_iff, LieSubmodule.top_lie_le_iff_le_normalizer, LieIdeal.topEquiv_apply, LieModule.maxNilpotentSubmodule_eq_top_of_isNilpotent, LieModule.lowerCentralSeriesLast_le_max_triv, RootPairing.GeckConstruction.ΟConjLieSubmodule_eq_top_iff, LieModule.mem_posFittingComp, LieSubmodule.map_incl_le, LieModule.ideal_oper_maxTrivSubmodule_eq_bot, LieModule.genWeightSpace_chainTopCoeff_add_one_zsmul_add, LieModule.isNilpotent_quotient_iff, LieModule.genWeightSpace_le_genWeightSpaceChain, LieSubmodule.coe_inf, LieSubmodule.eq_top_of_isIrreducible, LieModule.maxTrivEquiv_of_equiv_symm_eq_symm, LieSubmodule.normalizer_inf, LieSubmodule.Quotient.map_mk'_eq_bot_le, LieSubmodule.sSup_toSubmodule, LieModule.shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply, LieSubmodule.lieSpan_mono, LieSubmodule.lowerCentralSeries_eq_lcs_comap, LieSubmodule.lieSpan_eq, LieModuleHom.range_eq_top, LieModule.isNilpotent_iff_exists_ucs_eq_top, LieModule.traceForm_eq_sum_finrank_nsmul, LieSubmodule.wellFoundedLT_of_isArtinian, LieModule.exists_genWeightSpace_smul_add_eq_bot, LieSubmodule.Quotient.isCentralScalar, LieDerivation.IsKilling.rangeAdOrthogonal_carrier, LieSubmodule.mem_sup, LieModule.finite_genWeightSpace_ne_bot, LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal, LieIdeal.derivedSeries_eq_bot_iff, LieSubmodule.sSup_image_lieSpan_singleton, LieIdeal.comap_bracket_incl, LieModule.shiftedGenWeightSpace.instIsNilpotentSubtypeMemLieSubmoduleOfIsNoetherian, LieSubmodule.mem_idealizer, LieModule.isCompl_genWeightSpace_zero_posFittingComp, LieIdeal.killingForm_eq, LieSubmodule.lcs_le_iff, LieSubmodule.Quotient.surjective_mk', LieSubmodule.instIsAtomicOfIsArtinian, LieModule.isNilpotent_of_top_iff', LieModule.genWeightSpaceChain_def, LieSubmodule.ext_iff, LieModule.chainTopCoeff_add_one, LieSubmodule.coe_toEnd, LieAlgebra.InvariantForm.mem_orthogonal, LieSubmodule.Quotient.lieModuleHom_ext_iff, LieSubmodule.sInf_toSubmodule_eq_iInf, LieSubmodule.coe_neg, LieModule.le_max_triv_iff_bracket_eq_bot, LieModule.exists_nontrivial_weightSpace_of_isSolvable, LieSubmodule.coe_bracket, LieAlgebra.maxNilpotentIdeal_eq_top_of_isNilpotent, LieAlgebra.IsSemisimple.non_abelian_of_isAtom, LieAlgebra.abelian_of_le_center, LieSubmodule.wellFoundedGT_of_noetherian, LieModuleEquiv.ofTop_apply, LieModule.isNilpotent_toEnd_sub_algebraMap, LieSubmodule.sSup_toSubmodule_eq_iSup, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieSubmodule.ucs_le_of_normalizer_eq_self, LieIdeal.incl_idealRange, LieModule.eventually_genWeightSpace_smul_add_eq_bot, LieModule.zero_genWeightSpace_eq_top_of_nilpotent, LieSubmodule.inf_lie, LieSubmodule.coe_injective, LieSubmodule.lie_le_right, LieIdeal.comap_incl_self, LieSubmodule.incl_eq_val, LieSubmodule.gc_map_comap, LieSubmodule.instNontrivial, LieModule.weightSpace_le_genWeightSpace, LieModule.iSup_genWeightSpace_eq_top, LieModule.maxTrivEquiv_of_refl_eq_refl, LieSubmodule.Quotient.mk_eq_zero', LieSubalgebra.normalizer_eq_self_iff, LieSubmodule.nontrivial_iff_ne_bot, LieSubmodule.Quotient.mk_bracket, LieSubmodule.mk_eq_bot_iff, LieModule.map_lowerCentralSeries_le, LieModule.coe_lowerCentralSeries_eq_int, LieSubmodule.coe_toSubmodule, LieSubmodule.top_coe, LieSubmodule.nontrivial_iff, LieSubmodule.map_sup, LieAlgebra.radicalIsSolvable, LieModule.isNilpotent_iff_le_maxNilpotentSubmodule, LieModule.traceForm_genWeightSpace_eq, LieModule.instIsNilpotentSup, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, LieIdeal.lcs_zero, LieModule.instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian, LieModule.isTrivial_iff_max_triv_eq_top, LieModule.zero_lt_finrank_genWeightSpace, LieModule.zero_genWeightSpace_eq_top_of_nilpotent', LieModule.iSupIndep_genWeightSpace, LieModule.iSup_ucs_eq_genWeightSpace_zero, LieSubmodule.lieIdeal_oper_eq_tensor_map_range, LieSubmodule.codisjoint_toSubmodule, LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm, LieIdeal.isLieAbelian_of_trivial, LieSubmodule.coe_sInf, LieSubmodule.le_normalizer, LieSubmodule.Quotient.lieQuotientLieModule, LieSubmodule.iSup_toSubmodule_eq_top, LieSubmodule.lieIdeal_oper_eq_linear_span, LieModule.IsNilpotent.nilpotent_int, LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq, LieAlgebra.mem_corootSpace', LieSubmodule.mem_top, LieModule.posFittingCompOf_le_lowerCentralSeries, LieAlgebra.Extension.ringModuleOf_bracket_proj, LieAlgebra.abelian_derivedAbelianOfIdeal, LieSubmodule.mapOrderEmbedding_apply, LieModule.nontrivial_lowerCentralSeriesLast, LieSubmodule.lieIdeal_oper_eq_span, LieAlgebra.abelian_iff_derived_succ_eq_bot, LieSubmodule.coe_toEnd_pow, LieSubmodule.map_bot, LieSubmodule.add_eq_sup, LieSubmodule.lieSpan_le, LieModule.mem_genWeightSpaceOf, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, LieModule.iSupIndep_genWeightSpaceOf, LieModule.traceForm_eq_sum_finrank_nsmul_mul, LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieModule.coe_maxTrivEquiv_apply, LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter, instIsLieTowerSubtypeMemLieSubmodule_1, LieSubmodule.instIsNoetherianSubtypeMem, LieSubmodule.map_le_map_iff, LieSubmodule.mem_carrier, LieModule.eventually_iInf_lowerCentralSeries_eq, LieModule.posFittingCompOf_le_posFittingComp, LieSubmodule.lcs_succ, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, LieAlgebra.IsKilling.rootSpace_two_smul, LieSubmodule.incl_coe, LieSubmodule.map_le_iff_le_comap, LieAlgebra.mem_corootSpace, LieModule.iterate_toEnd_mem_lowerCentralSeries, LieAlgebra.isSolvableAdd, LieSubmodule.toSubmodule_eq_top, LieAlgebra.maxNilpotentIdeal_le_radical, LieAlgebra.maxNilpotentIdealIsNilpotent, LieModule.coe_maxTrivHom_apply, LieIdeal.coe_lcs_eq, LieSubmodule.gc_lcs_ucs, LieSubmodule.mem_lieSpan, LieSubmodule.instAddSubgroupClass, LieSubmodule.map_le_range, LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent, LieModule.map_posFittingComp_le, LieSubmodule.instLieModule, LieSubmodule.toSubmodule_eq_bot, LieModule.iSupIndep_genWeightSpace', LieAlgebra.derivedLength_eq_derivedLengthOfIdeal, LieSubmodule.Quotient.isNoetherian, LieSubmodule.lcs_le_self, instIsLieTowerSubtypeMemLieSubmodule, LieSubmodule.subsingleton_iff, LieAlgebra.Extension.twoCocycleOf_coe_coe, LieSubmodule.map_bracket_eq, LieSubmodule.Quotient.mk'_apply, LieSubmodule.comap_inf, LieSubmodule.injective_incl, LieSubmodule.le_comap_map, LieAlgebra.isSolvableBot, LieSubmodule.map_comap_incl, LieDerivation.maxTrivSubmodule_eq_bot_of_center_eq_bot, LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, LieModule.shiftedGenWeightSpace.shift_symm_apply, LieSubmodule.iSupIndep_toSubmodule, LieModule.injOn_genWeightSpace, LieAlgebra.LieIdeal.solvable_iff_le_radical, LieIdeal.incl_apply, LieSubmodule.baseChange_top, LieModule.posFittingComp_eq_bot_of_isNilpotent, Function.instIsSolvableSubtypeMemLieSubmodule, LieSubmodule.coe_iInf, LieSubmodule.ucs_bot_one, LieSubmodule.mem_normalizer, LieModuleHom.map_top, LieAlgebra.Extension.lie_toKer_apply, LieSubmodule.span_empty, LieSubmodule.lie_eq_bot_iff, LieModule.genWeightSpace_neg_add_chainBot, LieSubmodule.comap_incl_self, LieAlgebra.rootSpaceProduct_tmul, LieSubmodule.eq_bot_iff, LieSubmodule.coe_add, LieIdeal.ker_incl, LieModule.coe_maxTrivLinearMapEquivLieModuleHom, LieSubmodule.normalizer_bot_eq_maxTrivSubmodule, LieModule.genWeightSpace_add_chainTop, LieSubmodule.instIsModularLattice, LieIdeal.comap_incl_eq_bot, LieIdeal.inclusion_apply, LieSubmodule.mem_map, LieSubmodule.lie_coe_mem_lie, LieModule.coe_lowerCentralSeries_ideal_le, LieAlgebra.Extension.oneCochainOfTwoSplitting_apply, LieSubmodule.sInf_coe, LieAlgebra.isExtension_of_surjective, LieSubmodule.inf_toSubmodule, LieModuleEquiv.range_coe, LieModule.genWeightSpace_genWeightSpaceOf_map_incl, LieSubmodule.gc_top_lie_normalizer, LieSubmodule.mem_coe, LieSubmodule.inf_coe, LieModule.disjoint_genWeightSpace, LieModule.isCompl_genWeightSpaceOf_zero_posFittingCompOf, LieSubmodule.baseChange_bot
|