Basic

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

Statistics

Metric	Count
Definitions IsLieTower, LieAlgebra, toModule, LieEquiv, hasCoeToLieHom, hasCoeToLinearEquiv, instEquivLike, instInhabited, instOne, invFun, ofBijective, refl, toLieHom, toLinearEquiv, trans, LieHom, comp, id, instCoeLinearMapId, instFunLike, instInhabited, instOne, instZero, inverse, toLinearMap, LieModule, LieModuleEquiv, hasCoeToEquiv, hasCoeToLieModuleHom, hasCoeToLinearEquiv, instEquivLike, instInhabited, instOne, invFun, refl, toEquiv, toLieModuleHom, toLinearEquiv, trans, LieModuleHom, comp, hasNSMul, hasZSMul, id, instAdd, instAddCommGroup, instCoeOutLinearMapId, instFunLike, instInhabited, instModule, instNeg, instOne, instSMul, instSub, instZero, inverse, toLinearMap, LieRing, instLieAlgebra, toAddCommGroup, toBracket, toNonUnitalNonAssocRing, LieRingModule, compLieHom, toBracket, toEnd, instLieRingModule, instLieRingModule, lieRingSelfModule, «term_→ₗ⁅_,_⁆_», «term_→ₗ⁅_⁆_», «term_≃ₗ⁅_,_⁆_», «term_≃ₗ⁅_⁆_»	73
Theorems leibniz_lie, ext, ext_iff, lie_smul, toModule_injective, apply_symm_apply, bijective, coe_coe, coe_injective, coe_toLieHom, coe_toLinearEquiv, ext, ext_iff, injective, instLinearEquivClass, left_inv, map_lie, ofBijective_invFun, ofBijective_toFun, one_apply, refl_apply, refl_symm, right_inv, self_trans_symm, surjective, symm_apply_apply, symm_bijective, symm_symm, symm_trans, symm_trans_self, toLinearEquiv_injective, toLinearEquiv_mk, trans_apply, coe_comp, coe_id, coe_injective, coe_mk, coe_one, coe_toLinearMap, coe_zero, comp_apply, comp_id, congr_fun, ext, ext_iff, id_apply, id_comp, instLinearMapClass, lie_apply, map_add, map_lie, map_lie', map_neg, map_smul, map_sub, map_zero, mk_coe, one_apply, toFun_eq_coe, toLinearMap_comp, zero_apply, compLieHom, lie_smul, smul_lie, apply_eq_iff_eq_symm_apply, apply_symm_apply, coe_coe, coe_mk, coe_toLieModuleHom, coe_toLinearEquiv, ext, ext_iff, injective, instLinearEquivClass, left_inv, one_apply, refl_apply, right_inv, self_trans_symm, surjective, symm_apply_apply, symm_bijective, symm_symm, symm_trans, symm_trans_self, toEquiv_injective, toEquiv_mk, trans_apply, add_apply, coe_add, coe_comp, coe_id, coe_injective, coe_linear_mk, coe_mk, coe_neg, coe_nsmul, coe_smul, coe_sub, coe_toLinearMap, coe_zero, coe_zsmul, comp_apply, congr_fun, ext, ext_iff, id_apply, instLinearMapClass, map_add, map_lie, map_lie', map_lie₂, map_neg, map_smul, map_sub, map_zero, mk_coe, neg_apply, nsmul_apply, smul_apply, sub_apply, toLinearMap_comp, zero_apply, zsmul_apply, add_lie, leibniz_lie, lie_add, lie_self, add_lie, compLieHom_apply, leibniz_lie, lie_add, toEnd_apply_apply, instLieModule, instLieModule, lie_apply, add_lie, instIsLieTower, instLieModuleInt, instSubsingletonLieAlgebraRat, leibniz_lie, lieAlgebraSelfModule, lie_add, lie_jacobi, lie_lie, lie_neg, lie_nsmul, lie_self, lie_skew, lie_smul, lie_sub, lie_sum, lie_swap_lie, lie_zero, lie_zsmul, neg_lie, nsmul_lie, smul_lie, sub_lie, sum_lie, sum_lie_sum, zero_lie, zsmul_lie	163
Total	236

IsLieTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leibniz_lie 📖	mathematical	—	Bracket.bracket	—	—

LieAlgebra

Definitions

Name	Category	Theorems
toModule 📖	CompOp	459 math math: LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map, IsKilling.rootSystem_toLinearMap_apply, Extension.incl_apply_mem_ker, IsKilling.iInf_ker_weight_eq_bot, LieDerivation.lie_der_ad_eq_ad_der, LieSubalgebra.top_toSubmodule, LieDerivation.instNoetherian, LieDerivation.ad_apply_lieDerivation, LieDerivation.iterate_apply_lie, LieIdeal.map_bracket_le, LieDerivation.IsKilling.instIsKilling_range_ad, abelian_radical_of_hasTrivialRadical, IsKilling.restrict_killingForm_eq_sum, LieIdeal.comap_incl_eq_top, derivedLength_zero, LieSubmodule.lowerCentralSeries_tensor_eq_baseChange, LieIdeal.restrict_killingForm, LieIdeal.coe_bracket_of_module, LieModule.traceForm_eq_sum_genWeightSpaceOf, IsKilling.isCompl_ker_weight_span_coroot, finrank_engel, LieModule.traceForm_eq_sum_finrank_nsmul', LieSubalgebra.mem_map_submodule, isSolvable_iff_int, IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, IsKilling.rootSystem_coroot_apply, IsKilling.traceForm_cartan_nondegenerate, LieModule.derivedSeries_le_lowerCentralSeries, LieHom.mem_idealRange, isRegular_iff_natTrailingDegree_charpoly_eq_rank, LeftInvariantDerivation.left_invariant, LieSubmodule.bot_lie, LieDerivation.coe_sub_linearMap, LieIdeal.gc_map_comap, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieModule.instIsFaithfulMatrixForall, LieIdeal.map_comap_incl, LieDerivation.IsKilling.exists_eq_ad, LieSubalgebra.submodule_span_le_lieSpan, lieCharacterEquivLinearDual_apply, of_smul, coe_zeroRootSubalgebra, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, hasTrivialRadical_iff, IsKilling.corootSpace_eq_bot_iff, LieIdeal.incl_injective, LieDerivation.apply_lie_eq_add, LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap, IsSl2Triple.lie_lie_smul_f, IsSemisimple.booleanGenerators, derivedSeriesOfIdeal_succ_le, IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, LieSubmodule.lieIdeal_oper_eq_linear_span', instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieModule.Cohomology.twoCochain_alt, LieDerivation.commutator_apply, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieHom.quotKerEquivRange_toFun, LieRinehartAlgebra.Hom.anchor_derivation, IsKilling.apply_coroot_eq_cast', LieModule.traceForm_eq_zero_of_isNilpotent, LieIdeal.lowerCentralSeries_map_eq, derivedSeries_of_derivedLength_succ, LieModule.Cohomology.d₂₃_apply, LieIdeal.coe_killingCompl_top, LieModule.Cohomology.d₁₂_apply_apply, SpecialLinear.singleSubSingle_add_singleSubSingle, Extension.toKer_bracket, LieSubalgebra.toSubmodule_le_toSubmodule, non_trivial_center_of_isNilpotent, bracket_ofTwoCocycle, LieIdeal.instIsNilpotentSubtypeMemLieSubmoduleOfIsNilpotent, rank_le_natTrailingDegree_charpoly_ad, LieIdeal.coe_toLieSubalgebra, Derivation.bracket_eq_fun, LieSubalgebra.mem_toSubmodule, abelian_of_solvable_ideal_eq_bot_iff, LieIdeal.mem_killingCompl, ad_eq_lmul_left_sub_lmul_right, LieModule.traceForm_isSymm, LieDerivation.coe_neg_linearMap, LieDerivation.coe_smul_linearMap, abelian_radical_iff_solvable_is_abelian, LieModule.instIsTriangularizableSubtypeMemLieSubmodule, hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.sup_lie, LieSubalgebra.mem_carrier, FreeLieAlgebra.liftAux_map_smul, LieModule.LinearWeights.map_smul, LieSubalgebra.engel_carrier, LoopAlgebra.toFinsupp_symm_single, LieModule.Weight.coe_coe, LieModule.mem_ker, LieIdeal.le_killingCompl_top_of_isLieAbelian, LieModule.traceForm_lieSubalgebra_mk_right, IsKilling.chainLength_zero, self_module_ker_eq_center, lieAlgebraSelfModule, LieIdeal.incl_coe, Extension.lie_incl_mem_ker, radical_eq_top_of_isSolvable, coe_rootSpaceWeightSpaceProduct_tmul, IsKilling.invtSubmoduleToLieIdeal_top, LieIdeal.derivedSeries_map_le, LieHom.ker_eq_bot, IsKilling.coe_corootSpace_eq_span_singleton', IsSl2Triple.mem_toLieSubalgebra_iff, LeftInvariantDerivation.evalAt_coe, LieIdeal.incl_isIdealMorphism, LieSubalgebra.coe_normalizer_eq_normalizer, engel_isBot_of_isMin.lieCharpoly_map_eval, LieSubalgebra.coe_toSubmodule, rootSpaceProduct_def, lieEquivMatrix'_apply, LieRinehartAlgebra.toIsScalarTower, LieSubalgebra.sInf_toSubmodule, LieModule.lowerCentralSeries_succ, LieSubmodule.lie_le_inf, cartan_sup_iSup_rootSpace_eq_top, LieSubalgebra.coe_ad_pow, derivedSeriesOfIdeal_le_self, LieIdeal.lieModule, Derivation.instLieModule, IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieIdeal.subsingleton_of_bot, isSolvable_iff, lieCharacterEquivLinearDual_symm_apply, LieSubalgebra.mem_toLieSubmodule, LieIdeal.toLieSubalgebra_toSubmodule, Extension.lieModuleOf, instIsSolvableTensorProduct, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LinearMap.BilinForm.lieInvariant_iff, LieModule.Cohomology.twoCochain_skew, Matrix.instLieModuleForall, LieModule.traceForm_comm, IsKilling.killingForm_nondegenerate, derivedSeriesOfIdeal_succ, LieDerivation.IsKilling.killingForm_restrict_range_ad, IsSl2Triple.lie_h_e_smul, Extension.ringModuleOf_bracket, ad_nilpotent_of_nilpotent, IsSemisimple.sSup_atoms_eq_top, LieModule.rank_eq_natTrailingDegree, LieSubmodule.mem_baseChange_iff, DirectSum.lieAlgebraComponent_apply, IsKilling.chainLength_neg, IsSimple.isAtom_top, ad_pow_lie, LieModule.Cohomology.d₁₂_apply_coe_apply_apply, LieEquiv.right_inv, FreeLieAlgebra.liftAux_map_add, RootPairing.GeckConstruction.span_range_h'_eq_top, LieIdeal.isLieAbelian_iff, LieModule.Cohomology.mem_twoCochain_iff, instIsFaithfulOfHasTrivialRadical, LieModule.Weight.coe_toLinear_eq_zero_iff, IsKilling.coroot_mem_corootSpace, abelian_iff_derived_one_eq_bot, LieSubalgebra.toSubmodule_injective, LieIdeal.incl_range, Derivation.commutator_coe_linear_map, LieHom.toNonUnitalAlgHom_toFun, LieModule.exists_nontrivial_weightSpace_of_isNilpotent, LieIdeal.map_mono, IsKilling.apply_coroot_eq_cast, LieSubalgebra.coe_incl', LieModule.Cohomology.d₁₂_apply_apply_ofTrivial, FreeLieAlgebra.liftAux_map_mul, IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, JacobsonNoether.exist_pow_eq_zero_of_le, LieSubmodule.lie_comm, center_le_radical, coe_lowerCentralSeries_ideal_quot_eq, RootPairing.GeckConstruction.span_range_h_le_range_diagonal, LieModule.Weight.isZero_neg, LieModule.instIsNilpotentTensor, LieDerivation.coe_zero_linearMap, LieHom.ker_le_comap, zero_rootSpace_eq_top_of_nilpotent, LieModule.lie_traceForm_eq_zero, LieDerivation.leibniz_lie, IsKilling.corootForm_rootSystem_eq_killing, LieModule.trace_comp_toEnd_genWeightSpace_eq, LieIdeal.comap_bracket_le, RootPairing.GeckConstruction.instIsIrreducible, killingForm_apply_apply, LieDerivation.lie_apply, LieIdeal.map_lowerCentralSeries_le, smulCommClass, LieSubalgebra.mem_engel_iff, lie_smul, LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra, hasTrivialRadical_iff_no_solvable_ideals, LieModule.Cohomology.mem_twoCocycle_iff, LieIdeal.map_sup_ker_eq_map', LieModule.traceForm_eq_zero_of_isTrivial, derivedSeriesOfIdeal_antitone, LieSubmodule.lie_baseChange, LieModule.toModuleHom_apply, IsExtension.ker_eq_bot, LieSubmodule.top_lie_le_iff_le_normalizer, LieIdeal.topEquiv_apply, IsSolvable.solvable_int, derivedSeries_baseChange, derivedSeriesOfIdeal_add_le_add, LieDerivation.toLinearMapLieHom_injective, FreeLieAlgebra.liftAux_spec, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, LieDerivation.ad_isIdealMorphism, derivedSeries_def, LieIdeal.coe_map_of_surjective, LieDerivation.lie_coe_lieDerivation_apply, smul_lie, LieModule.toEnd_lie, ExtendScalars.bracket_tmul, LieModule.Cohomology.add_apply_apply, IsKilling.biSup_corootSpace_eq_top, LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero, LieHom.toFun_eq_coe, IsKilling.disjoint_ker_weight_corootSpace, LoopAlgebra.toFinsupp_single_tmul, ad_apply, LieIdeal.isCompl_killingCompl, LieHom.instLinearMapClass, LieModule.traceForm_eq_sum_finrank_nsmul, conj_ad_apply, LieSubmodule.tmul_mem_baseChange_of_mem, toModule_injective, Extension.ofTwoCocycle_proj_apply, LieDerivation.IsKilling.rangeAdOrthogonal_carrier, LieHom.quotKerEquivRange_invFun, LieSubalgebra.toSubmodule_eq_bot, LieSubalgebra.coe_ofLe, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal, LieIdeal.derivedSeries_eq_bot_iff, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, Extension.bracket, LieIdeal.comap_bracket_incl, IsKilling.span_weight_isNonZero_eq_top, IsKilling.chainTopCoeff_add_chainBotCoeff, LieSubmodule.mem_idealizer, LieIdeal.killingForm_eq, center_eq_bot, LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit, rootSpace_comap_eq_genWeightSpace, LieModule.isFaithful_iff_ker_eq_bot, isLieAbelian_iff_center_eq_top, LieModule.traceForm_lieSubalgebra_mk_left, LieDerivation.commutator_coe_linear_map, LieModule.Cohomology.smul_apply_apply, UniversalEnvelopingAlgebra.ι_apply, LieHom.coe_toLinearMap, LieModule.Cohomology.instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain, LieModule.toEnd_pow_lie, restrict_killingForm, Extension.ofTwoCocycle_incl_apply, LieIdeal.coe_derivedSeries_eq_int, LieIdeal.map_comap_bracket_eq, LieModule.toEnd_baseChange, LieHom.idealRange_eq_map, LieModule.le_max_triv_iff_bracket_eq_bot, LieSubalgebra.coe_toLieSubmodule, LieModule.smul_lie, IsKilling.coroot_neg, LieModule.exists_nontrivial_weightSpace_of_isSolvable, maxNilpotentIdeal_eq_top_of_isNilpotent, LieHom.idealRange_eq_lieSpan_range, LieIdeal.comap_mono, LieHom.toNonUnitalAlgHom_apply, SpecialLinear.val_single, LoopAlgebra.residuePairing_apply_apply, lieEquivMatrix'_symm_apply, LieSubalgebra.instIsNoetherianSubtypeMem, IsKilling.ideal_eq_bot_of_isLieAbelian, SpecialLinear.singleSubSingle_sub_singleSubSingle, IsKilling.biSup_corootSubmodule_eq_cartan, LieIdeal.incl_idealRange, LieSubmodule.inf_lie, HasTrivialRadical.radical_eq_bot, rank_le_finrank_engel, LieIdeal.comap_incl_self, LieDerivation.IsKilling.range_ad_eq_top, LieHom.range_toSubmodule, isScalarTower, IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieDerivation.lie_ad, IsSimple.instIsIrreducible, LieHom.mem_ker, LieSubalgebra.normalizer_eq_self_iff, IsKilling.rootSystem_pairing_apply, LieSubmodule.Quotient.mk_bracket, IsKilling.killingCompl_top_eq_bot, IsKilling.orthogonal_span_coroot_eq_ker, IsKilling.cartanEquivDual_apply_apply, LieDerivation.leibniz', rank_le_finrank, LieIdeal.map_comap_eq, LieSubalgebra.toSubmodule_eq_top, LieIdeal.comap_map_le, IsKilling.coroot_eq_zero_iff, hasTrivialRadical_iff_no_abelian_ideals, isFaithful_self_iff, LieHom.range_subset_idealRange, radicalIsSolvable, LieModule.traceForm_genWeightSpace_eq, LieModule.traceForm_apply_apply, IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, LieIdeal.mem_comap, LieIdeal.map_bracket_eq, LieModule.Cohomology.twoCochain_val_apply, ext_iff, LieSubmodule.lieIdeal_oper_eq_tensor_map_range, LieIdeal.map_le_iff_le_comap, LieSubalgebra.inf_toSubmodule, LieIdeal.isLieAbelian_of_trivial, LieIdeal.top_toLieSubalgebra, Submodule.exists_lieSubalgebra_coe_eq_iff, rank_eq_natTrailingDegree, LieModule.traceForm_apply_lie_apply, IsKilling.chainBotCoeff_le_chainLength, LieSubmodule.lieIdeal_oper_eq_linear_span, LieEquiv.toLinearEquiv_injective, LieDerivation.IsKilling.ad_apply_eq_zero_iff, mem_corootSpace', derivedSeries_lt_top_of_solvable, LieIdeal.derivedSeries_succ_eq_top_iff, ad_lie, derivedSeries_of_bot_eq_bot, LieHom.toLinearMap_comp, Extension.ringModuleOf_bracket_proj, abelian_derivedAbelianOfIdeal, LeftInvariantDerivation.evalAt_mul, LieHom.map_le_idealRange, LieSubmodule.lieIdeal_oper_eq_span, abelian_iff_derived_succ_eq_bot, LieHom.map_lie', isNilpotent_range_ad_iff, IsKilling.traceForm_coroot, LieIdeal.map_le, LieDerivation.coe_add_linearMap, LieModule.traceForm_eq_sum_finrank_nsmul_mul, toLieSubmodule_le_rootSpace_zero, IsKilling.coroot_zero, nilpotent_ad_of_nilpotent_algebra, Derivation.commutator_apply, instIsLieAbelianSubtypeMemLieSubmoduleCenter, instIsLieTowerSubtypeMemLieSubmodule_1, LieSubalgebra.coe_lieSpan_submodule_eq_iff, LieModule.Weight.isNonZero_neg, derivedSeriesOfIdeal_baseChange, center_le_maxNilpotentIdeal, IsKilling.chainBotCoeff_add_chainTopCoeff, LieSubmodule.lcs_succ, mem_zeroRootSubalgebra, Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, LieHom.mem_idealRange_iff, isRegular_iff_finrank_engel_eq_rank, IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra, LieSubalgebra.instIsScalarTowerSubtypeMem, ExtendScalars.instLieModule, mem_corootSpace, LieModule.Cohomology.mem_twoCocycle_iff_of_trivial, isSolvableAdd, isSolvable_tensorProduct_iff, LieIdeal.toSubmodule_killingCompl, maxNilpotentIdeal_le_radical, HasTrivialRadical.eq_bot_of_isSolvable, LieRinehartAlgebra.instDerivation, LieHom.ker_toSubmodule, maxNilpotentIdealIsNilpotent, IsKilling.chainTopCoeff_le_chainLength, LieIdeal.coe_lcs_eq, LieDerivation.coe_ad_apply_eq_ad_apply, SpecialLinear.val_singleSubSingle, isNilpotent_iff_forall, ad_ker_eq_bot_of_hasTrivialRadical, IsKilling.span_weight_eq_top, LieSubalgebra.bot_toSubmodule, LieModule.traceForm_flip, LieDerivation.ad_ker_eq_center, LieEquiv.left_inv, LieModule.traceForm_apply_lie_apply', LieDerivation.mem_ad_idealRange_iff, LieDerivation.instLinearMapClass, derivedLength_eq_derivedLengthOfIdeal, LieHom.le_ker_iff, IsSemisimple.sSupIndep_isAtom, isNilpotent_ad_of_isNilpotent, instIsLieTowerSubtypeMemLieSubmodule, LieModule.Weight.toLinear_neg, LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, LieSubmodule.coe_baseChange, isSolvableBot, IsKilling.ker_killingForm_eq_bot, LieDerivation.coeFn_coe, LieIdeal.comap_bracket_eq, LieSubalgebra.instSMulMemClass, LieIdeal.solvable_iff_le_radical, LieDerivation.toFun_eq_coe, LieModule.Cohomology.d₂₃_comp_d₁₂, LieIdeal.incl_apply, LieSubmodule.baseChange_top, IsSolvable.solvable, Function.instIsSolvableSubtypeMemLieSubmodule, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, of_symm_smul, LieDerivation.iterate_apply_lie', ad_ker_eq_self_module_ker, LieIdeal.map_sup_ker_eq_map, LieEquiv.ofBijective_invFun, IsSimple.isAtom_iff_eq_top, DirectSum.toLieAlgebra_apply, LieModule.range_traceForm_le_span_weight, Extension.lie_toKer_apply, IsKilling.corootSpace_zero_eq_bot, ExtendScalars.map_apply_tmul, rootSpaceProduct_tmul, LieModule.traceForm_lieInvariant, LieIdeal.ker_incl, LieSubmodule.lie_le_left, LieIdeal.lcs_top, LieRinehartAlgebra.toLieModule, SpecialLinear.singleSubSingle_sub_singleSubSingle', IsKilling.rootSystem_root_apply, LieIdeal.comap_incl_eq_bot, LieIdeal.map_eq_bot_iff, LieSubalgebra.instIsArtinianSubtypeMem, LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra, LieSubalgebra.smul_mem, LieSubmodule.lie_coe_mem_lie, LieModule.coe_lowerCentralSeries_ideal_le, LieModule.Weight.coe_neg, LieIdeal.comap_toSubmodule, LieIdeal.map_comap_le, UniversalEnvelopingAlgebra.lift_ι_apply', LieModule.Weight.instLinearMapClass, isExtension_of_surjective, IsKilling.coe_corootSpace_eq_span_singleton, LieIdeal.idealizer_eq_normalizer, LieRinehartAlgebra.instLieRinehartRingDerivation, LieEquiv.instLinearEquivClass, IsSimple.eq_bot_or_eq_top, LieModule.ker_eq_bot, LieSubalgebra.coe_ad, LieIdeal.map_sup, LieModule.toEnd_matrix, LieModule.Weight.toLinear_apply, LieHom.idealRange_eq_top_of_surjective, LieSubmodule.gc_top_lie_normalizer, IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, LieHom.toNonUnitalAlgHom_injective, LieEquiv.coe_toLinearEquiv, LieDerivation.ad_apply_apply, LieSubmodule.baseChange_bot, LeftInvariantDerivation.evalAt_apply, LieSubalgebra.ad_comp_incl_eq, killingForm_of_equiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup Module.toDistribMulAction toModule	—	—	—
ext_iff 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup Module.toDistribMulAction toModule	—	ext
lie_smul 📖	mathematical	—	Bracket.bracket LieRing.toBracket SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup Module.toDistribMulAction toModule	—	—
toModule_injective 📖	mathematical	—	LieAlgebra Rat.commRing Module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup toModule	—	—

LieEquiv

Definitions

Name	Category	Theorems
hasCoeToLieHom 📖	CompOp	—
hasCoeToLinearEquiv 📖	CompOp	—
instEquivLike 📖	CompOp	49 math math: skewAdjointMatricesLieSubalgebraEquivTranspose_apply, map_lie, Matrix.lieConj_apply, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, skewAdjointLieSubalgebraEquiv_apply, LieSubalgebra.equivOfLe_apply, one_apply, skewAdjointLieSubalgebraEquiv_symm_apply, coe_injective, LieHom.quotKerEquivRange_toFun, LieHom.equivRangeOfInjective_apply, LieAlgebra.Extension.toKer_bracket, LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, lieEquivMatrix'_apply, LieDerivation.exp_map_apply, ext_iff, LieAlgebra.Extension.ringModuleOf_bracket, ofEq_apply, trans_apply, ofSubalgebras_apply, Matrix.reindexLieEquiv_apply, LieAlgebra.LieEquiv.ofCoboundary_toFun, lieSubalgebraMap_apply, AlgEquiv.toLieEquiv_symm_apply, Matrix.lieConj_symm_apply, apply_symm_apply, LieIdeal.topEquiv_apply, LinearEquiv.lieConj_apply, LieAlgebra.conj_ad_apply, symm_apply_apply, LieAlgebra.Extension.bracket, RootPairing.GeckConstruction.ωConj_toFun, lieEquivMatrix'_symm_apply, LieSubalgebra.topEquiv_apply, ofSubalgebras_symm_apply, RootPairing.GeckConstruction.ωConj_mem_of_mem, ofInjective_apply, LieAlgebra.Extension.ringModuleOf_bracket_proj, ofBijective_toFun, coe_coe, skewAdjointMatricesLieSubalgebraEquiv_apply, AlgEquiv.toLieEquiv_apply, refl_apply, LieAlgebra.Extension.lie_toKer_apply, coe_toLieHom, LieAlgebra.Extension.oneCochainOfTwoSplitting_apply, instLinearEquivClass, coe_toLinearEquiv, LieAlgebra.killingForm_of_equiv_apply
instInhabited 📖	CompOp	—
instOne 📖	CompOp	1 math math: one_apply
invFun 📖	CompOp	6 math math: right_inv, LieHom.quotKerEquivRange_invFun, RootPairing.GeckConstruction.ωConj_invFun, LieAlgebra.LieEquiv.ofCoboundary_invFun, left_inv, ofBijective_invFun
ofBijective 📖	CompOp	2 math math: ofBijective_toFun, ofBijective_invFun
refl 📖	CompOp	4 math math: refl_symm, symm_trans_self, self_trans_symm, refl_apply
toLieHom 📖	CompOp	10 math math: bijective, injective, LieSubalgebra.mem_map_submodule, right_inv, lieSubalgebraMap_apply, surjective, coe_coe, left_inv, coe_toLieHom, LieModule.toEnd_matrix
toLinearEquiv 📖	CompOp	7 math math: LieSubalgebra.mem_map_submodule, LieDerivation.exp_apply, LieAlgebra.conj_ad_apply, toLinearEquiv_injective, toLinearEquiv_mk, LieAlgebra.Extension.twoCocycleOf_coe_coe, coe_toLinearEquiv
trans 📖	CompOp	4 math math: symm_trans, trans_apply, symm_trans_self, self_trans_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_symm_apply 📖	mathematical	—	DFunLike.coe LieEquiv EquivLike.toFunLike instEquivLike symm	—	LinearEquiv.apply_symm_apply RingHomInvPair.ids
bijective 📖	mathematical	—	Function.Bijective DFunLike.coe LieHom LieHom.instFunLike toLieHom	—	LinearEquiv.bijective RingHomInvPair.ids
coe_coe 📖	mathematical	—	DFunLike.coe LieHom LieHom.instFunLike toLieHom LieEquiv EquivLike.toFunLike instEquivLike	—	—
coe_injective 📖	mathematical	—	LieEquiv DFunLike.coe EquivLike.toFunLike instEquivLike	—	RingHomInvPair.ids LinearEquiv.coe_injective toLinearEquiv_injective
coe_toLieHom 📖	mathematical	—	DFunLike.coe LieHom LieHom.instFunLike toLieHom LieEquiv EquivLike.toFunLike instEquivLike	—	—
coe_toLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule EquivLike.toFunLike LinearEquiv.instEquivLike toLinearEquiv LieEquiv instEquivLike	—	RingHomInvPair.ids
ext 📖	—	DFunLike.coe LieEquiv EquivLike.toFunLike instEquivLike	—	—	coe_injective
ext_iff 📖	mathematical	—	DFunLike.coe LieEquiv EquivLike.toFunLike instEquivLike	—	ext
injective 📖	mathematical	—	DFunLike.coe LieHom LieHom.instFunLike toLieHom	—	LinearEquiv.injective RingHomInvPair.ids
instLinearEquivClass 📖	mathematical	—	LinearEquivClass LieEquiv CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule instEquivLike	—	RingHomInvPair.ids coe_toLinearEquiv map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass RingHom.id_apply
left_inv 📖	mathematical	—	invFun AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieAlgebra.toModule LieHom.toLinearMap toLieHom	—	—
map_lie 📖	mathematical	—	DFunLike.coe LieEquiv EquivLike.toFunLike instEquivLike Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule	—	LieHom.map_lie
ofBijective_invFun 📖	mathematical	Function.Bijective DFunLike.coe LieHom LieHom.instFunLike	invFun ofBijective LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm LinearEquiv.ofBijective LieHom.toLinearMap	—	—
ofBijective_toFun 📖	mathematical	Function.Bijective DFunLike.coe LieHom LieHom.instFunLike	LieEquiv EquivLike.toFunLike instEquivLike ofBijective	—	—
one_apply 📖	mathematical	—	DFunLike.coe LieEquiv EquivLike.toFunLike instEquivLike instOne	—	—
refl_apply 📖	mathematical	—	DFunLike.coe LieEquiv EquivLike.toFunLike instEquivLike refl	—	—
refl_symm 📖	mathematical	—	symm refl	—	—
right_inv 📖	mathematical	—	invFun AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieAlgebra.toModule LieHom.toLinearMap toLieHom	—	—
self_trans_symm 📖	mathematical	—	trans symm refl	—	ext symm_apply_apply
surjective 📖	mathematical	—	DFunLike.coe LieHom LieHom.instFunLike toLieHom	—	LinearEquiv.surjective RingHomInvPair.ids
symm_apply_apply 📖	mathematical	—	DFunLike.coe LieEquiv EquivLike.toFunLike instEquivLike symm	—	LinearEquiv.symm_apply_apply RingHomInvPair.ids
symm_bijective 📖	mathematical	—	Function.Bijective LieEquiv symm	—	Function.bijective_iff_has_inverse symm_symm
symm_symm 📖	mathematical	—	symm	—	—
symm_trans 📖	mathematical	—	symm trans	—	—
symm_trans_self 📖	mathematical	—	trans symm refl	—	self_trans_symm
toLinearEquiv_injective 📖	mathematical	—	LieEquiv LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule toLinearEquiv	—	RingHomInvPair.ids
toLinearEquiv_mk 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieAlgebra.toModule LieHom.toLinearMap	toLinearEquiv RingHomInvPair.ids	—	RingHomInvPair.ids
trans_apply 📖	mathematical	—	DFunLike.coe LieEquiv EquivLike.toFunLike instEquivLike trans	—	—

LieHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	8 math math: comp_apply, id_comp, coe_comp, UniversalEnvelopingAlgebra.lift_symm_apply, comp_id, AlgHom.toLieHom_comp, toLinearMap_comp, UniversalEnvelopingAlgebra.hom_ext_iff
id 📖	CompOp	6 math math: coe_id, AlgHom.toLieHom_id, id_comp, id_apply, comp_id, LieModule.toEnd_module_end
instCoeLinearMapId 📖	CompOp	—
instFunLike 📖	CompOp	184 math math: LieEquiv.bijective, coe_zero, LieAlgebra.Extension.incl_apply_mem_ker, LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, LieDerivation.lie_der_ad_eq_ad_der, LieDerivation.ad_apply_lieDerivation, LieSubalgebra.inclusion_apply, ext_iff, zero_apply, congr_fun, LieModule.toEnd_pow_apply_map, LieEquiv.injective, LieModule.trace_toEnd_eq_zero_of_mem_lcs, surjective_rangeRestrict, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LieAlgebra.finrank_engel, LieSubalgebra.equivOfLe_apply, mem_idealRange, LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, LieSubalgebra.toEnd_eq, LieDerivation.IsKilling.exists_eq_ad, LieModule.isNilpotent_toEnd_genWeightSpace_zero, LieIdeal.incl_injective, coe_id, LieModule.trace_toEnd_genWeightSpace, UniversalEnvelopingAlgebra.lift_unique, LieModule.shiftedGenWeightSpace.toEnd_eq, FreeLieAlgebra.of_comp_lift, one_apply, LieSubmodule.Quotient.toEnd_comp_mk', LieModule.mem_posFittingCompOf, mem_range_self, LieAlgebra.Extension.toKer_bracket, LieAlgebra.rank_le_natTrailingDegree_charpoly_ad, LieSubmodule.lie_top_eq_of_span_sup_eq_top, LieAlgebra.ad_eq_lmul_left_sub_lmul_right, LieModule.isNilpotent_toEnd_of_isNilpotent, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.coe_map_toEnd_le, LieModule.mem_genWeightSpace, UniversalEnvelopingAlgebra.ι_comp_lift, FreeLieAlgebra.lift_comp_of, LieAlgebra.Extension.incl_injective, LieAlgebra.Extension.lie_incl_mem_ker, LieSubalgebra.toEnd_mk, ker_eq_bot, LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, LieModule.coe_genWeightSpaceOf_zero, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, map_lie, LieSubmodule.traceForm_eq_zero_of_isTrivial, LieModule.weight_vector_multiplication, LieSubalgebra.coe_ad_pow, LieRinehartAlgebra.Hom.map_smul_apply', RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, LieModule.isFaithful_iff, LieAlgebra.Extension.ringModuleOf_bracket, LieSubalgebra.coe_inclusion, LieSubmodule.toEnd_comp_subtype_mem, LieAlgebra.ad_nilpotent_of_nilpotent, DirectSum.lieAlgebraComponent_apply, LieAlgebra.ad_pow_lie, comp_apply, LieModule.isNilpotent_toEnd_of_isNilpotent₂, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, toNonUnitalAlgHom_toFun, LieModule.exists_forall_pow_toEnd_eq_zero, DirectSum.lieAlgebraOf_apply, LieDerivation.IsKilling.ad_mem_orthogonal_of_mem_orthogonal, JacobsonNoether.exist_pow_eq_zero_of_le, rangeRestrict_apply, LieRingModule.compLieHom_apply, LieSubmodule.toEnd_restrict_eq_toEnd, LieIdeal.coe_inclusion, UniversalEnvelopingAlgebra.lift_ι_apply, coe_range, FreeLieAlgebra.lift_unique, LieModule.IsFaithful.injective_toEnd, LieSubalgebra.mem_comap, LieIdeal.inclusion_injective, range_eq_top, killingForm_apply_apply, LieSubalgebra.mem_engel_iff, LieModule.iterate_toEnd_mem_lowerCentralSeries₂, coe_comp, IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat, LieModule.toEnd_eq_iff, id_apply, LieModule.isNilpotent_toEnd_of_mem_rootSpace, range_coe, LieDerivation.toLinearMapLieHom_injective, LieEquiv.surjective, LieModule.toEnd_lie, toFun_eq_coe, isIdealMorphism_iff, LieAlgebra.ad_apply, LieAlgebra.toEnd_pow_apply_mem, instLinearMapClass, LieModule.coe_genWeightSpace_of_top, LieAlgebra.lieCharacter_apply_of_mem_derived, LieAlgebra.conj_ad_apply, LieAlgebra.Extension.ofTwoCocycle_proj_apply, LieSubalgebra.inclusion_injective, coe_mk, LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, UniversalEnvelopingAlgebra.ι_apply, coe_toLinearMap, LieModule.toEnd_pow_lie, LieSubmodule.coe_toEnd, LieModule.toEnd_apply_apply, LieAlgebra.Extension.ofTwoCocycle_incl_apply, coe_injective, LieModule.commute_toEnd_of_mem_center_right, coe_one, LieModule.toEnd_baseChange, FreeLieAlgebra.hom_ext_iff, toNonUnitalAlgHom_apply, LieModule.isNilpotent_iff_forall, LieModule.isNilpotent_toEnd_sub_algebraMap, AlgHom.coe_toLieHom, IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, LieDerivation.lie_ad, LieAlgebra.Extension.proj_incl, mem_ker, LieSubalgebra.coe_incl, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieModule.toEnd_eq_zero_iff, LieAlgebra.isNilpotent_ad_of_mem_rootSpace, LieModule.traceForm_apply_apply, LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, LieIdeal.mem_comap, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, LieRinehartAlgebra.Hom.map_smul_apply, LieModule.maxGenEigenSpace_toEnd_eq_top, FreeLieAlgebra.lift_symm_apply, LieDerivation.IsKilling.ad_apply_eq_zero_iff, LieSubalgebra.mem_map, LieAlgebra.ad_lie, LieModule.isNilpotent_iff_forall', LieAlgebra.Extension.ringModuleOf_bracket_proj, LieSubmodule.coe_toEnd_pow, LieModule.mem_genWeightSpaceOf, LieDerivation.injective_ad_of_center_eq_bot, LieIdeal.map_le, LieAlgebra.nilpotent_ad_of_nilpotent_algebra, LieAlgebra.Extension.proj_surjective, mem_range, FreeLieAlgebra.lift_of_apply, LieAlgebra.mem_zeroRootSubalgebra, mem_idealRange_iff, LieRinehartAlgebra.Hom.apply_lie', LieModule.iterate_toEnd_mem_lowerCentralSeries, LieAlgebra.lieCharacter_apply_lie, LieDerivation.coe_ad_apply_eq_ad_apply, LieAlgebra.lieCharacter_apply_lie', LieEquiv.coe_coe, LieAlgebra.isNilpotent_iff_forall, LieDerivation.mem_ad_idealRange_iff, le_ker_iff, LieAlgebra.isNilpotent_ad_of_isNilpotent, LieRinehartAlgebra.Hom.toLinearMap'_apply, AlgHom.toLieHom_apply, LieIdeal.incl_apply, LieModule.commute_toEnd_of_mem_center_left, DirectSum.toLieAlgebra_apply, LieAlgebra.Extension.lie_toKer_apply, LieEquiv.coe_toLieHom, LieAlgebra.ExtendScalars.map_apply_tmul, range_eq_ker_iff, LieIdeal.inclusion_apply, UniversalEnvelopingAlgebra.lift_ι_apply', LieIdeal.mem_map, LieRinehartAlgebra.Hom.apply_lie, LieModule.Weight.hasEigenvalueAt, LieModule.rank_le_natTrailingDegree_charpoly_ad, LieSubalgebra.coe_ad, LieModule.toEnd_pow_comp_lieHom, LieDerivation.ad_apply_apply, LieSubalgebra.ad_comp_incl_eq
instInhabited 📖	CompOp	—
instOne 📖	CompOp	2 math math: one_apply, coe_one
instZero 📖	CompOp	2 math math: coe_zero, zero_apply
inverse 📖	CompOp	—
toLinearMap 📖	CompOp	21 math math: LieAlgebra.lieCharacterEquivLinearDual_apply, quotKerEquivRange_toFun, LieIdeal.incl_coe, LieIdeal.map_toSubmodule, LieModule.rank_eq_natTrailingDegree, LieEquiv.right_inv, LieModule.trace_comp_toEnd_genWeightSpace_eq, LieIdeal.coe_map_of_surjective, toFun_eq_coe, quotKerEquivRange_invFun, coe_toLinearMap, range_toSubmodule, LieAlgebra.rank_eq_natTrailingDegree, toLinearMap_comp, map_lie', ker_toSubmodule, LieEquiv.left_inv, LieEquiv.ofBijective_invFun, DirectSum.toLieAlgebra_apply, LieIdeal.comap_toSubmodule, LieSubalgebra.ad_comp_incl_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe LieHom instFunLike comp	—	—
coe_id 📖	mathematical	—	DFunLike.coe LieHom instFunLike id	—	—
coe_injective 📖	mathematical	—	LieHom DFunLike.coe instFunLike	—	—
coe_mk 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddHom.toFun SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction LieAlgebra.toModule DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.id LinearMap.toAddHom Bracket.bracket LieRingModule.toBracket lieRingSelfModule	LieHom instFunLike	—	—
coe_one 📖	mathematical	—	DFunLike.coe LieHom instFunLike instOne	—	—
coe_toLinearMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike toLinearMap LieHom instFunLike	—	—
coe_zero 📖	mathematical	—	DFunLike.coe LieHom instFunLike instZero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	—
comp_apply 📖	mathematical	—	DFunLike.coe LieHom instFunLike comp	—	—
comp_id 📖	mathematical	—	comp id	—	—
congr_fun 📖	mathematical	—	DFunLike.coe LieHom instFunLike	—	—
ext 📖	—	DFunLike.coe LieHom instFunLike	—	—	coe_injective
ext_iff 📖	mathematical	—	DFunLike.coe LieHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe LieHom instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	—
instLinearMapClass 📖	mathematical	—	LinearMapClass LieHom CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule instFunLike	—	coe_toLinearMap map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass
lie_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Bracket.bracket LieRingModule.toBracket LinearMap.addCommGroup LinearMap.instLieRingModule SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
map_add 📖	mathematical	—	DFunLike.coe	—	map_add
map_lie 📖	mathematical	—	DFunLike.coe LieHom instFunLike Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule	—	map_lie'
map_lie' 📖	mathematical	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieAlgebra.toModule toLinearMap Bracket.bracket LieRingModule.toBracket lieRingSelfModule	—	—
map_neg 📖	mathematical	—	DFunLike.coe SubNegMonoid.toNeg AddGroup.toSubNegMonoid SubtractionMonoid.toSubNegMonoid	—	map_neg
map_smul 📖	mathematical	—	DFunLike.coe	—	map_smul
map_sub 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid SubtractionMonoid.toSubNegMonoid	—	map_sub
map_zero 📖	mathematical	—	DFunLike.coe	—	map_zero
mk_coe 📖	—	DFunLike.coe LieHom instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddHom.toFun SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction LieAlgebra.toModule RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.id LinearMap.toAddHom Bracket.bracket LieRingModule.toBracket lieRingSelfModule	—	—	ext
one_apply 📖	mathematical	—	DFunLike.coe LieHom instFunLike instOne	—	—
toFun_eq_coe 📖	mathematical	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieAlgebra.toModule toLinearMap DFunLike.coe LieHom instFunLike	—	—
toLinearMap_comp 📖	mathematical	—	toLinearMap comp LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
zero_apply 📖	mathematical	—	DFunLike.coe LieHom instFunLike instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	—

LieModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compLieHom 📖	mathematical	—	LieModule LieRingModule.compLieHom	—	map_smul SemilinearMapClass.toMulActionSemiHomClass LieHom.instLinearMapClass smul_lie lie_smul
lie_smul 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket 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 AddCommGroup.toAddCommMonoid	—	—
smul_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket 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	—	—

LieModuleEquiv

Definitions

Name	Category	Theorems
hasCoeToEquiv 📖	CompOp	—
hasCoeToLieModuleHom 📖	CompOp	—
hasCoeToLinearEquiv 📖	CompOp	—
instEquivLike 📖	CompOp	18 math math: injective, refl_apply, apply_eq_iff_eq_symm_apply, symm_apply_apply, TensorProduct.LieModule.coe_liftLie_eq_lift_coe, trans_apply, instLinearEquivClass, coe_toLinearEquiv, TensorProduct.LieModule.lift_apply, ofTop_apply, coe_mk, ext_iff, apply_symm_apply, LieModule.coe_maxTrivEquiv_apply, coe_toLieModuleHom, coe_coe, surjective, one_apply
instInhabited 📖	CompOp	—
instOne 📖	CompOp	1 math math: one_apply
invFun 📖	CompOp	2 math math: left_inv, right_inv
refl 📖	CompOp	4 math math: refl_apply, LieModule.maxTrivEquiv_of_refl_eq_refl, symm_trans_self, self_trans_symm
toEquiv 📖	CompOp	2 math math: toEquiv_mk, toEquiv_injective
toLieModuleHom 📖	CompOp	9 math math: LieSubmodule.orderIsoMapComap_apply, left_inv, LieSubmodule.orderIsoMapComap_symm_apply, LieModule.map_genWeightSpace_eq, LieModule.map_posFittingComp_eq, coe_toLieModuleHom, coe_coe, right_inv, range_coe
toLinearEquiv 📖	CompOp	1 math math: coe_toLinearEquiv
trans 📖	CompOp	4 math math: symm_trans, trans_apply, symm_trans_self, self_trans_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_iff_eq_symm_apply 📖	mathematical	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.apply_eq_iff_eq_symm_apply
apply_symm_apply 📖	mathematical	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike symm	—	LinearEquiv.apply_symm_apply RingHomInvPair.ids
coe_coe 📖	mathematical	—	DFunLike.coe LieModuleHom LieModuleHom.instFunLike toLieModuleHom LieModuleEquiv EquivLike.toFunLike instEquivLike	—	—
coe_mk 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieModuleHom.toLinearMap	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike LieModuleHom LieModuleHom.instFunLike	—	—
coe_toLieModuleHom 📖	mathematical	—	DFunLike.coe LieModuleHom LieModuleHom.instFunLike toLieModuleHom LieModuleEquiv EquivLike.toFunLike instEquivLike	—	—
coe_toLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike LinearEquiv.instEquivLike toLinearEquiv LieModuleEquiv instEquivLike	—	RingHomInvPair.ids
ext 📖	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike	—	—	toEquiv_injective Equiv.ext
ext_iff 📖	mathematical	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike	—	ext
injective 📖	mathematical	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike	—	Equiv.injective
instLinearEquivClass 📖	mathematical	—	LinearEquivClass LieModuleEquiv CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instEquivLike	—	RingHomInvPair.ids coe_toLinearEquiv map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass RingHom.id_apply
left_inv 📖	mathematical	—	invFun AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieModuleHom.toLinearMap toLieModuleHom	—	—
one_apply 📖	mathematical	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike instOne	—	—
refl_apply 📖	mathematical	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike refl	—	—
right_inv 📖	mathematical	—	invFun AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieModuleHom.toLinearMap toLieModuleHom	—	—
self_trans_symm 📖	mathematical	—	trans symm refl	—	ext symm_apply_apply
surjective 📖	mathematical	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike	—	Equiv.surjective
symm_apply_apply 📖	mathematical	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike symm	—	LinearEquiv.symm_apply_apply RingHomInvPair.ids
symm_bijective 📖	mathematical	—	Function.Bijective LieModuleEquiv symm	—	Function.bijective_iff_has_inverse symm_symm
symm_symm 📖	mathematical	—	symm	—	—
symm_trans 📖	mathematical	—	symm trans	—	—
symm_trans_self 📖	mathematical	—	trans symm refl	—	ext apply_symm_apply
toEquiv_injective 📖	mathematical	—	LieModuleEquiv Equiv toEquiv	—	—
toEquiv_mk 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieModuleHom.toLinearMap	toEquiv DFunLike.coe LieModuleHom LieModuleHom.instFunLike	—	—
trans_apply 📖	mathematical	—	DFunLike.coe LieModuleEquiv EquivLike.toFunLike instEquivLike trans	—	—

LieModuleHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	7 math math: comp_apply, toLinearMap_comp, comp_ker_incl, LieSubmodule.Quotient.lieModuleHom_ext_iff, coe_comp, LieSubmodule.lieIdeal_oper_eq_tensor_map_range, LieSubmodule.map_comp
hasNSMul 📖	CompOp	2 math math: nsmul_apply, coe_nsmul
hasZSMul 📖	CompOp	2 math math: zsmul_apply, coe_zsmul
id 📖	CompOp	4 math math: ker_id, coe_id, LieSubmodule.map_id, id_apply
instAdd 📖	CompOp	2 math math: coe_add, add_apply
instAddCommGroup 📖	CompOp	6 math math: TensorProduct.LieModule.liftLie_apply, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom, TensorProduct.LieModule.coe_liftLie_eq_lift_coe, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm, LieModule.coe_maxTrivLinearMapEquivLieModuleHom
instCoeOutLinearMapId 📖	CompOp	—
instFunLike 📖	CompOp	60 math math: mem_range, TensorProduct.LieModule.liftLie_apply, LieSubmodule.coe_map, LieModule.toEnd_pow_apply_map, LieSubmodule.Quotient.mk_eq_zero, zsmul_apply, LieSubmodule.mem_comap, ker_eq_bot, LieModuleEquiv.toEquiv_mk, coe_mk, instLinearMapClass, coe_id, LieSubmodule.incl_apply, mem_ker, coe_toLinearMap, comp_apply, coe_smul, coe_zsmul, coe_injective, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, smul_apply, nsmul_apply, coe_neg, TensorProduct.LieModule.map_tmul, coe_restrictLie, LieSubalgebra.coe_incl', TensorProduct.LieModule.coe_liftLie_eq_lift_coe, coe_range, LieSubmodule.coe_inclusion, LieModule.toModuleHom_apply, zero_apply, neg_apply, range_eq_top, coe_add, LieSubmodule.Quotient.surjective_mk', coe_comp, LieModuleEquiv.coe_mk, LieSubmodule.incl_eq_val, coe_nsmul, LieSubmodule.inclusion_apply, id_apply, coe_zero, LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm, add_apply, LieSubmodule.mem_map_of_mem, LieSubmodule.inclusion_injective, map_lie, LieModuleEquiv.coe_toLieModuleHom, coe_sub, LieModule.coe_maxTrivHom_apply, sub_apply, ext_iff, LieModuleEquiv.coe_coe, congr_fun, LieSubmodule.Quotient.mk'_apply, LieSubmodule.injective_incl, LieAlgebra.rootSpaceProduct_tmul, LieModule.coe_maxTrivLinearMapEquivLieModuleHom, LieSubmodule.mem_map, map_lie₂
instInhabited 📖	CompOp	—
instModule 📖	CompOp	6 math math: TensorProduct.LieModule.liftLie_apply, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom, TensorProduct.LieModule.coe_liftLie_eq_lift_coe, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm, LieModule.coe_maxTrivLinearMapEquivLieModuleHom
instNeg 📖	CompOp	2 math math: coe_neg, neg_apply
instOne 📖	CompOp	—
instSMul 📖	CompOp	2 math math: coe_smul, smul_apply
instSub 📖	CompOp	2 math math: coe_sub, sub_apply
instZero 📖	CompOp	3 math math: comp_ker_incl, zero_apply, coe_zero
inverse 📖	CompOp	—
toLinearMap 📖	CompOp	18 math math: LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom, LieSubmodule.Quotient.toEnd_comp_mk', coe_toLinearMap, LieModuleEquiv.left_inv, toSubmodule_range, LieSubmodule.toSubmodule_map, LieModule.weight_vector_multiplication, toLinearMap_comp, TensorProduct.LieModule.coe_liftLie_eq_lift_coe, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, coe_linear_mk, ker_toSubmodule, TensorProduct.LieModule.toLinearMap_map, LieSubmodule.toSubmodule_comap, map_lie', LieSubmodule.incl_coe, LieModuleEquiv.right_inv, LieModule.toEnd_pow_comp_lieHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	—
coe_add 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instAdd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	—
coe_comp 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike comp	—	—
coe_id 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike id	—	—
coe_injective 📖	mathematical	—	LieModuleHom DFunLike.coe instFunLike	—	—
coe_linear_mk 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Bracket.bracket LieRingModule.toBracket	toLinearMap	—	—
coe_mk 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Bracket.bracket LieRingModule.toBracket	DFunLike.coe LieModuleHom instFunLike LinearMap LinearMap.instFunLike	—	—
coe_neg 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instNeg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_nsmul 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike hasNSMul AddMonoid.toNatSMul Pi.addMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
coe_smul 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instSMul Function.hasSMul 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 AddCommGroup.toAddCommMonoid	—	—
coe_sub 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
coe_toLinearMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike toLinearMap LieModuleHom instFunLike	—	—
coe_zero 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instZero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_zsmul 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike hasZSMul SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
comp_apply 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike comp	—	—
congr_fun 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike	—	—
ext 📖	—	DFunLike.coe LieModuleHom instFunLike	—	—	coe_injective
ext_iff 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike id	—	—
instLinearMapClass 📖	mathematical	—	LinearMapClass LieModuleHom CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike	—	coe_toLinearMap map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass
map_add 📖	mathematical	—	DFunLike.coe	—	map_add
map_lie 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike Bracket.bracket LieRingModule.toBracket	—	map_lie'
map_lie' 📖	mathematical	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring toLinearMap Bracket.bracket LieRingModule.toBracket	—	—
map_lie₂ 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LieModuleHom LinearMap.addCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instLieRingModule instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	smulCommClass_self map_lie sub_add_cancel
map_neg 📖	mathematical	—	DFunLike.coe SubNegMonoid.toNeg AddGroup.toSubNegMonoid SubtractionMonoid.toSubNegMonoid	—	map_neg
map_smul 📖	mathematical	—	DFunLike.coe	—	map_smul
map_sub 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid SubtractionMonoid.toSubNegMonoid	—	map_sub
map_zero 📖	mathematical	—	DFunLike.coe	—	map_zero
mk_coe 📖	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring toLinearMap Bracket.bracket LieRingModule.toBracket	—	—	—
neg_apply 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
nsmul_apply 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike hasNSMul AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
smul_apply 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instSMul 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 AddCommGroup.toAddCommMonoid	—	—
sub_apply 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
toLinearMap_comp 📖	mathematical	—	toLinearMap comp LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
zero_apply 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
zsmul_apply 📖	mathematical	—	DFunLike.coe LieModuleHom instFunLike hasZSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—

LieRing

Definitions

Name	Category	Theorems
instLieAlgebra 📖	CompOp	7 math math: LieAlgebra.isSolvable_iff_int, instLieModuleInt, LieModule.isNilpotent_iff_int, LieAlgebra.IsSolvable.solvable_int, LieIdeal.coe_derivedSeries_eq_int, LieModule.coe_lowerCentralSeries_eq_int, LieModule.IsNilpotent.nilpotent_int
toAddCommGroup 📖	CompOp	555 math math: LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map, LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieHom.coe_zero, LieAlgebra.Extension.incl_apply_mem_ker, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, LieDerivation.lie_der_ad_eq_ad_der, LieSubalgebra.top_toSubmodule, LieDerivation.instNoetherian, LieRinehartRing.lie_smul_eq_mul, DirectSum.bracket_apply, LieDerivation.ad_apply_lieDerivation, LieDerivation.iterate_apply_lie, LieIdeal.map_bracket_le, Function.Surjective.isLieAbelian, LieDerivation.IsKilling.instIsKilling_range_ad, LieAlgebra.abelian_radical_of_hasTrivialRadical, LieHom.zero_apply, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, LieIdeal.comap_incl_eq_top, LieAlgebra.derivedLength_zero, LieSubmodule.lowerCentralSeries_tensor_eq_baseChange, LieSubalgebra.isLieAbelian_lieSpan_iff, LieIdeal.restrict_killingForm, LieAlgebra.Orthogonal.mem_so, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, zsmul_lie, LieEquiv.map_lie, LieIdeal.coe_bracket_of_module, LieModule.traceForm_eq_sum_genWeightSpaceOf, Matrix.isSkewAdjoint_bracket, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, LieAlgebra.finrank_engel, LieModule.traceForm_eq_sum_finrank_nsmul', LieSubalgebra.mem_map_submodule, LieAlgebra.isSolvable_iff_int, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, LieModule.derivedSeries_le_lowerCentralSeries, LieHom.mem_idealRange, LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank, LieSubmodule.bot_lie, LieDerivation.coe_sub_linearMap, LieIdeal.gc_map_comap, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieModule.instIsFaithfulMatrixForall, LieIdeal.map_comap_incl, LieDerivation.IsKilling.exists_eq_ad, LieSubalgebra.submodule_span_le_lieSpan, LieAlgebra.lieCharacterEquivLinearDual_apply, LieAlgebra.of_smul, LieAlgebra.coe_zeroRootSubalgebra, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, LieAlgebra.hasTrivialRadical_iff, leibniz_lie, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, LieIdeal.incl_injective, LieDerivation.apply_lie_eq_add, LieSubalgebra.bot_coe, LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap, IsSl2Triple.lie_lie_smul_f, LieAlgebra.IsSemisimple.booleanGenerators, lie_add, LieAlgebra.derivedSeriesOfIdeal_succ_le, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, LieSubalgebra.mem_bot, LieSubmodule.lieIdeal_oper_eq_linear_span', LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieModule.Cohomology.twoCochain_alt, LieDerivation.commutator_apply, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieModule.traceForm_eq_zero_of_isNilpotent, LieIdeal.lowerCentralSeries_map_eq, LieAlgebra.derivedSeries_of_derivedLength_succ, LieModule.Cohomology.d₂₃_apply, LieIdeal.coe_killingCompl_top, LieModule.Cohomology.d₁₂_apply_apply, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, LieAlgebra.Extension.toKer_bracket, LieSubalgebra.toSubmodule_le_toSubmodule, LieAlgebra.non_trivial_center_of_isNilpotent, DirectSum.lie_of_of_ne, LieAlgebra.bracket_ofTwoCocycle, LieIdeal.instIsNilpotentSubtypeMemLieSubmoduleOfIsNilpotent, LieAlgebra.rank_le_natTrailingDegree_charpoly_ad, LieIdeal.coe_toLieSubalgebra, Derivation.bracket_eq_fun, DirectSum.lie_of, LieSubalgebra.mem_toSubmodule, LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff, LieIdeal.mem_killingCompl, LieAlgebra.ad_eq_lmul_left_sub_lmul_right, LieModule.traceForm_isSymm, LieDerivation.coe_neg_linearMap, LieDerivation.coe_smul_linearMap, LieAlgebra.abelian_radical_iff_solvable_is_abelian, two_nsmul_lie_lmul_lmul_add_add_eq_zero, LieModule.instIsTriangularizableSubtypeMemLieSubmodule, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.sup_lie, commutative_ring_iff_abelian_lie_ring, LieSubalgebra.mem_carrier, FreeLieAlgebra.liftAux_map_smul, LieModule.LinearWeights.map_smul, LieModule.genWeightSpaceChain_neg, LieSubalgebra.engel_carrier, LieAlgebra.LoopAlgebra.toFinsupp_symm_single, LieRinehartRing.leibniz_mul_right, LieModule.Weight.coe_coe, LieRingModule.toEnd_apply_apply, LieModule.mem_ker, lie_abelian_iff_equiv_lie_abelian, lie_apply, LieIdeal.le_killingCompl_top_of_isLieAbelian, LieModule.traceForm_lieSubalgebra_mk_right, LieAlgebra.IsKilling.chainLength_zero, LieAlgebra.self_module_ker_eq_center, lieAlgebraSelfModule, LieIdeal.incl_coe, LieSubalgebra.ideal_in_normalizer, LieAlgebra.Extension.lie_incl_mem_ker, LieAlgebra.radical_eq_top_of_isSolvable, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, LieIdeal.derivedSeries_map_le, LieHom.ker_eq_bot, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', IsSl2Triple.mem_toLieSubalgebra_iff, LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff, LieIdeal.incl_isIdealMorphism, LieSubalgebra.coe_normalizer_eq_normalizer, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, LieSubalgebra.coe_toSubmodule, LieAlgebra.rootSpaceProduct_def, LieHom.map_lie, lieEquivMatrix'_apply, LieRinehartAlgebra.toIsScalarTower, LieSubalgebra.sInf_toSubmodule, LieModule.instLinearWeightsOfIsLieAbelian, LieModule.lowerCentralSeries_succ, LieSubmodule.lie_le_inf, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, LieSubalgebra.coe_ad_pow, LieAlgebra.derivedSeriesOfIdeal_le_self, LieIdeal.lieModule, Derivation.instLieModule, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, Function.Injective.isLieAbelian, LieIdeal.subsingleton_of_bot, LieAlgebra.isSolvable_iff, LieAlgebra.lieCharacterEquivLinearDual_symm_apply, LieSubalgebra.add_mem, LieSubalgebra.mem_toLieSubmodule, LieRinehartAlgebra.Hom.map_smul_apply', LieIdeal.toLieSubalgebra_toSubmodule, LieAlgebra.Extension.lieModuleOf, LieAlgebra.instIsSolvableTensorProduct, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LinearMap.BilinForm.lieInvariant_iff, LieModule.Cohomology.twoCochain_skew, Matrix.instLieModuleForall, LieModule.traceForm_comm, LieAlgebra.IsKilling.killingForm_nondegenerate, LieAlgebra.derivedSeriesOfIdeal_succ, LieDerivation.IsKilling.killingForm_restrict_range_ad, IsSl2Triple.lie_h_e_smul, LieAlgebra.Extension.ringModuleOf_bracket, LieAlgebra.ad_nilpotent_of_nilpotent, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, LieModule.rank_eq_natTrailingDegree, LieSubmodule.mem_baseChange_iff, DirectSum.lieAlgebraComponent_apply, LieAlgebra.IsKilling.chainLength_neg, lie_self, LieAlgebra.IsSimple.isAtom_top, LieAlgebra.ad_pow_lie, LieModule.Cohomology.d₁₂_apply_coe_apply_apply, LieEquiv.right_inv, RootPairing.GeckConstruction.span_range_h'_eq_top, LieDerivation.map_sub, LieIdeal.isLieAbelian_iff, LieModule.Cohomology.mem_twoCochain_iff, LieAlgebra.instIsFaithfulOfHasTrivialRadical, LieModule.Weight.coe_toLinear_eq_zero_iff, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieAlgebra.abelian_iff_derived_one_eq_bot, LieSubalgebra.toSubmodule_injective, LieIdeal.incl_range, Derivation.commutator_coe_linear_map, LieModule.exists_nontrivial_weightSpace_of_isNilpotent, LieIdeal.map_mono, LieAlgebra.IsKilling.apply_coroot_eq_cast, LieSubalgebra.coe_incl', LieModule.Cohomology.d₁₂_apply_apply_ofTrivial, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', FreeLieAlgebra.liftAux_map_mul, DirectSum.lieAlgebraOf_apply, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, JacobsonNoether.exist_pow_eq_zero_of_le, LieSubmodule.lie_comm, LieAlgebra.center_le_radical, LieAlgebra.SpecialLinear.sl_bracket, coe_lowerCentralSeries_ideal_quot_eq, LieModule.Weight.isZero_neg, LieModule.instIsNilpotentTensor, LieDerivation.coe_zero_linearMap, LieHom.ker_le_comap, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieModule.lie_traceForm_eq_zero, neg_lie, LieDerivation.leibniz_lie, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, of_associative_ring_bracket, LieModule.trace_comp_toEnd_genWeightSpace_eq, RootPairing.GeckConstruction.ω_mul_h, LieIdeal.comap_bracket_le, RootPairing.GeckConstruction.instIsIrreducible, killingForm_apply_apply, LieDerivation.lie_apply, LieIdeal.map_lowerCentralSeries_le, LieAlgebra.smulCommClass, LieSubalgebra.mem_engel_iff, LieAlgebra.lie_smul, LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra, LieAlgebra.hasTrivialRadical_iff_no_solvable_ideals, LieModule.isFaithful_iff', two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add, LieModule.Cohomology.mem_twoCocycle_iff, LieIdeal.map_sup_ker_eq_map', LieModule.traceForm_eq_zero_of_isTrivial, LieAlgebra.derivedSeriesOfIdeal_antitone, LieSubmodule.lie_baseChange, LieAlgebra.Orthogonal.s_as_blocks, LieModule.toModuleHom_apply, LieAlgebra.IsExtension.ker_eq_bot, LieSubmodule.top_lie_le_iff_le_normalizer, LieIdeal.topEquiv_apply, lie_skew, LieAlgebra.IsSolvable.solvable_int, LieAlgebra.derivedSeries_baseChange, LieAlgebra.derivedSeriesOfIdeal_add_le_add, LieDerivation.toLinearMapLieHom_injective, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, LieRingModule.add_lie, Matrix.lie_apply, LieDerivation.ad_isIdealMorphism, LieAlgebra.derivedSeries_def, LieIdeal.coe_map_of_surjective, LieDerivation.lie_coe_lieDerivation_apply, smul_lie, LieModule.toEnd_lie, LieAlgebra.ExtendScalars.bracket_tmul, LieModule.Cohomology.add_apply_apply, LieSubalgebra.instIsLieTowerSubtypeMem, sum_lie, LieAlgebra.of_zero, LieRinehartRing.leibniz_smul_right, IsSl2Triple.symm, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieSubalgebra.coe_bracket, lie_self, LieHom.toFun_eq_coe, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieHom.isIdealMorphism_iff, LieAlgebra.LoopAlgebra.toFinsupp_single_tmul, LieAlgebra.ad_apply, LieIdeal.isCompl_killingCompl, LieHom.instLinearMapClass, lie_jacobi, LieModule.traceForm_eq_sum_finrank_nsmul, LieAlgebra.conj_ad_apply, LieSubmodule.tmul_mem_baseChange_of_mem, LieAlgebra.toModule_injective, LieAlgebra.Extension.ofTwoCocycle_proj_apply, LieDerivation.IsKilling.rangeAdOrthogonal_carrier, LieHom.quotKerEquivRange_invFun, LieSubalgebra.toSubmodule_eq_bot, LieSubalgebra.coe_ofLe, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal, LieIdeal.derivedSeries_eq_bot_iff, LieAlgebra.Extension.bracket, LieIdeal.comap_bracket_incl, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, LieSubmodule.mem_idealizer, LieModule.LinearWeights.map_add, LieIdeal.killingForm_eq, LieAlgebra.center_eq_bot, LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit, LieAlgebra.rootSpace_comap_eq_genWeightSpace, LieModule.isFaithful_iff_ker_eq_bot, LieAlgebra.of_add, LieAlgebra.isLieAbelian_iff_center_eq_top, LieModule.traceForm_lieSubalgebra_mk_left, LieDerivation.commutator_coe_linear_map, LieModule.Cohomology.smul_apply_apply, LieModule.LinearWeights.map_lie, DirectSum.lie_of_same, UniversalEnvelopingAlgebra.ι_apply, LieHom.coe_toLinearMap, LieModule.Cohomology.instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain, LieModule.toEnd_pow_lie, LieAlgebra.restrict_killingForm, LieAlgebra.Extension.ofTwoCocycle_incl_apply, LieIdeal.coe_derivedSeries_eq_int, LieIdeal.map_comap_bracket_eq, LieModule.toEnd_baseChange, LieHom.idealRange_eq_map, LieModule.le_max_triv_iff_bracket_eq_bot, LieSubalgebra.coe_toLieSubmodule, LieModule.smul_lie, RootPairing.GeckConstruction.f_lie_v_ne, LieAlgebra.IsKilling.coroot_neg, LieAlgebra.matrix_trace_commutator_zero, LieModule.exists_nontrivial_weightSpace_of_isSolvable, LieSubalgebra.mem_normalizer_iff', LieAlgebra.maxNilpotentIdeal_eq_top_of_isNilpotent, LieHom.idealRange_eq_lieSpan_range, LieIdeal.comap_mono, RootPairing.GeckConstruction.e_lie_v_ne, LieAlgebra.SpecialLinear.val_single, add_lie, LieAlgebra.LoopAlgebra.residuePairing_apply_apply, lieEquivMatrix'_symm_apply, LieSubalgebra.instIsNoetherianSubtypeMem, LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, LieSubalgebra.engel_zero, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieIdeal.incl_idealRange, LieSubmodule.inf_lie, LieAlgebra.HasTrivialRadical.radical_eq_bot, LieModule.chainTop_neg, LieSubalgebra.exists_lieIdeal_coe_eq_iff, LieAlgebra.rank_le_finrank_engel, LieModule.chainBot_neg, LieIdeal.comap_incl_self, LieDerivation.IsKilling.range_ad_eq_top, LieHom.range_toSubmodule, LieModule.Weight.apply_lie, LieAlgebra.isScalarTower, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.of_symm_nsmul, LieDerivation.lie_ad, LieAlgebra.IsSimple.instIsIrreducible, LieAlgebra.Extension.proj_incl, LieHom.mem_ker, LieSubalgebra.normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, Matrix.lie_transpose, LieSubmodule.Quotient.mk_bracket, LieAlgebra.IsKilling.killingCompl_top_eq_bot, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, zero_lie, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieDerivation.leibniz', LieDerivation.map_neg, LieModule.toEnd_eq_zero_iff, LieAlgebra.rank_le_finrank, LieIdeal.map_comap_eq, LieSubalgebra.toSubmodule_eq_top, LieIdeal.comap_map_le, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals, LieAlgebra.isFaithful_self_iff, LieHom.range_subset_idealRange, LieAlgebra.radicalIsSolvable, LieModule.traceForm_genWeightSpace_eq, LieSubalgebra.coe_zero_iff_zero, LieModule.traceForm_apply_apply, LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, LieIdeal.mem_comap, LieAlgebra.of_symm_zero, LieIdeal.map_bracket_eq, LieModule.Cohomology.twoCochain_val_apply, LieAlgebra.ext_iff, LieRinehartAlgebra.Hom.map_smul_apply, LieSubmodule.lieIdeal_oper_eq_tensor_map_range, LieIdeal.map_le_iff_le_comap, RootPairing.GeckConstruction.lie_e_lie_f_apply, LieSubalgebra.inf_toSubmodule, LieIdeal.isLieAbelian_of_trivial, LieSubalgebra.sub_mem, LieIdeal.top_toLieSubalgebra, Submodule.exists_lieSubalgebra_coe_eq_iff, LieAlgebra.rank_eq_natTrailingDegree, LieModule.traceForm_apply_lie_apply, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieSubmodule.lieIdeal_oper_eq_linear_span, LieEquiv.toLinearEquiv_injective, LieDerivation.IsKilling.ad_apply_eq_zero_iff, LieAlgebra.mem_corootSpace', LieAlgebra.derivedSeries_lt_top_of_solvable, LieIdeal.derivedSeries_succ_eq_top_iff, LieAlgebra.ad_lie, LieAlgebra.derivedSeries_of_bot_eq_bot, LieHom.toLinearMap_comp, RootPairing.GeckConstruction.f_lie_v_same, LieSubalgebra.zero_mem, LieAlgebra.Extension.ringModuleOf_bracket_proj, IsSl2Triple.lie_h_f_nsmul, LieAlgebra.abelian_derivedAbelianOfIdeal, LieHom.map_le_idealRange, LieSubmodule.lieIdeal_oper_eq_span, LieAlgebra.abelian_iff_derived_succ_eq_bot, LieHom.map_lie', sum_lie_sum, LieAlgebra.isNilpotent_range_ad_iff, LieDerivation.apply_lie_eq_sub, LieAlgebra.IsKilling.traceForm_coroot, LieIdeal.map_le, LieDerivation.coe_add_linearMap, IsSl2Triple.lie_h_e_nsmul, LieModule.chainBotCoeff_neg, LieModule.traceForm_eq_sum_finrank_nsmul_mul, LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieAlgebra.nilpotent_ad_of_nilpotent_algebra, LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter, instIsLieTowerSubtypeMemLieSubmodule_1, LieSubalgebra.coe_lieSpan_submodule_eq_iff, IsSl2Triple.symm_iff, LieModule.Weight.isNonZero_neg, LieAlgebra.derivedSeriesOfIdeal_baseChange, LieAlgebra.center_le_maxNilpotentIdeal, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieSubmodule.lcs_succ, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, LieHom.mem_idealRange_iff, LieAlgebra.isRegular_iff_finrank_engel_eq_rank, LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra, LieSubalgebra.instIsScalarTowerSubtypeMem, LieAlgebra.ExtendScalars.instLieModule, LieRinehartAlgebra.Hom.apply_lie', LieAlgebra.mem_corootSpace, LieModule.Cohomology.mem_twoCocycle_iff_of_trivial, LieAlgebra.isSolvableAdd, LieAlgebra.isSolvable_tensorProduct_iff, LieIdeal.toSubmodule_killingCompl, LieAlgebra.maxNilpotentIdeal_le_radical, LieAlgebra.lieCharacter_apply_lie, LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable, LieHom.ker_toSubmodule, LieAlgebra.maxNilpotentIdealIsNilpotent, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieIdeal.coe_lcs_eq, LieDerivation.coe_ad_apply_eq_ad_apply, LieAlgebra.lieCharacter_apply_lie', LieAlgebra.of_symm_add, LieAlgebra.SpecialLinear.val_singleSubSingle, LieAlgebra.isNilpotent_iff_forall, LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical, nsmul_lie, LieAlgebra.IsKilling.span_weight_eq_top, LieSubalgebra.bot_toSubmodule, LieModule.traceForm_flip, LieDerivation.ad_ker_eq_center, LieEquiv.left_inv, LieModule.traceForm_apply_lie_apply', LieDerivation.mem_ad_idealRange_iff, LieDerivation.instLinearMapClass, LieAlgebra.derivedLength_eq_derivedLengthOfIdeal, LieHom.le_ker_iff, LieAlgebra.IsSemisimple.sSupIndep_isAtom, LieAlgebra.isNilpotent_ad_of_isNilpotent, instIsLieTowerSubtypeMemLieSubmodule, LieModule.Weight.toLinear_neg, LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, LieSubmodule.coe_baseChange, LieModule.chainTopCoeff_neg, LieAlgebra.isSolvableBot, LieAlgebra.IsKilling.ker_killingForm_eq_bot, LieRinehartAlgebra.Hom.toLinearMap'_apply, LieDerivation.coeFn_coe, LieIdeal.comap_bracket_eq, LieSubalgebra.instSMulMemClass, LieAlgebra.LieIdeal.solvable_iff_le_radical, lie_lie, LieDerivation.toFun_eq_coe, LieModule.Cohomology.d₂₃_comp_d₁₂, LieIdeal.incl_apply, LieSubmodule.baseChange_top, LieAlgebra.IsSolvable.solvable, Function.instIsSolvableSubtypeMemLieSubmodule, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.IsSimple.non_abelian, LieAlgebra.of_symm_smul, LieSubalgebra.instIsCentralScalarSubtypeMem, LieDerivation.iterate_apply_lie', LieAlgebra.ad_ker_eq_self_module_ker, LieIdeal.map_sup_ker_eq_map, LieEquiv.ofBijective_invFun, IsSl2Triple.lie_e_f, LieAlgebra.IsSimple.isAtom_iff_eq_top, DirectSum.toLieAlgebra_apply, LieModule.range_traceForm_le_span_weight, LieAlgebra.Extension.lie_toKer_apply, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, sub_lie, LieModule.genWeightSpace_neg_add_chainBot, RootPairing.GeckConstruction.lie_e_f_mul_ω, LieAlgebra.ExtendScalars.map_apply_tmul, LieHom.range_eq_ker_iff, LieAlgebra.rootSpaceProduct_tmul, LieModule.traceForm_lieInvariant, LieSubalgebra.mem_normalizer_iff, LieIdeal.ker_incl, LieSubmodule.lie_le_left, LieIdeal.lcs_top, LieRinehartAlgebra.toLieModule, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.IsKilling.rootSystem_root_apply, LieIdeal.comap_incl_eq_bot, LieIdeal.map_eq_bot_iff, LieSubalgebra.instIsArtinianSubtypeMem, LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra, LieSubalgebra.smul_mem, LieSubmodule.lie_coe_mem_lie, LieModule.coe_lowerCentralSeries_ideal_le, LieModule.Weight.coe_neg, LieIdeal.comap_toSubmodule, LieIdeal.map_comap_le, UniversalEnvelopingAlgebra.lift_ι_apply', LieSubalgebra.eq_bot_iff, RootPairing.GeckConstruction.e_lie_u, LieRinehartAlgebra.Hom.apply_lie, LieModule.Weight.instLinearMapClass, LieAlgebra.isExtension_of_surjective, LieSubalgebra.instAddSubgroupClass, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, LieIdeal.idealizer_eq_normalizer, LieEquiv.instLinearEquivClass, LieAlgebra.IsSimple.eq_bot_or_eq_top, LieModule.ker_eq_bot, LieSubalgebra.coe_ad, LieIdeal.map_sup, LieModule.toEnd_matrix, LieModule.Weight.toLinear_apply, LieSubalgebra.lie_mem, LieHom.idealRange_eq_top_of_surjective, add_lie, LieSubmodule.gc_top_lie_normalizer, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, LieEquiv.coe_toLinearEquiv, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra, LieDerivation.ad_apply_apply, LieSubmodule.baseChange_bot, LieSubalgebra.ad_comp_incl_eq, LieAlgebra.of_nsmul, LieAlgebra.killingForm_of_equiv_apply
toBracket 📖	CompOp	8 math math: instIsLieTower, leibniz_lie, lie_add, lie_self, LieAlgebra.lie_smul, lie_self, add_lie, LieRingModule.leibniz_lie
toNonUnitalNonAssocRing 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_lie 📖	mathematical	—	Bracket.bracket toBracket AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup toAddCommGroup	—	—
leibniz_lie 📖	mathematical	—	Bracket.bracket toBracket AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup toAddCommGroup	—	—
lie_add 📖	mathematical	—	Bracket.bracket toBracket AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup toAddCommGroup	—	—
lie_self 📖	mathematical	—	Bracket.bracket toBracket AddMonoid.toZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup toAddCommGroup	—	—

LieRingModule

Definitions

Name	Category	Theorems
compLieHom 📖	CompOp	2 math math: compLieHom_apply, LieModule.compLieHom
toBracket 📖	CompOp	202 math math: Submodule.exists_lieSubmodule_coe_eq_iff, LieModule.trivial_iff_lower_central_eq_bot, instIsLieTower, LieRinehartRing.lie_smul_eq_mul, DirectSum.bracket_apply, LieDerivation.ad_apply_lieDerivation, LieDerivation.iterate_apply_lie, Function.Surjective.isLieAbelian, LieAlgebra.abelian_radical_of_hasTrivialRadical, LinearMap.BilinForm.isSkewAdjoint_bracket, LieSubalgebra.isLieAbelian_lieSpan_iff, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, zsmul_lie, LieEquiv.map_lie, LieIdeal.coe_bracket_of_module, Matrix.isSkewAdjoint_bracket, DirectSum.lie_module_bracket_apply, lie_sum, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieDerivation.apply_lie_eq_add, IsSl2Triple.lie_lie_smul_f, LieSubmodule.lie_le_iff, LieModule.instIsTrivialOfSubsingleton', LieModule.trivial_iff_le_maximal_trivial, LieSubmodule.lieIdeal_oper_eq_linear_span', LieDerivation.inner_apply_apply, LieModule.instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule, LieAlgebra.derivedSeries_of_derivedLength_succ, LieModule.Cohomology.d₂₃_apply, LieModule.mem_weightSpace, LieModule.Cohomology.d₁₂_apply_apply, lie_smul, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right, LieAlgebra.Extension.toKer_bracket, DirectSum.lie_of_of_ne, LieAlgebra.bracket_ofTwoCocycle, Derivation.bracket_eq_fun, DirectSum.lie_of, LieAlgebra.abelian_radical_iff_solvable_is_abelian, two_nsmul_lie_lmul_lmul_add_add_eq_zero, commutative_ring_iff_abelian_lie_ring, lie_neg, LieRinehartRing.leibniz_mul_right, toEnd_apply_apply, LieModule.mem_ker, LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff, lie_abelian_iff_equiv_lie_abelian, LieRing.lie_apply, LieSubalgebra.ideal_in_normalizer, LieAlgebra.Extension.lie_incl_mem_ker, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, IsSl2Triple.mem_toLieSubalgebra_iff, LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff, LieSubalgebra.coe_bracket_of_module, LieHom.map_lie, Function.Injective.isLieAbelian, LieModule.lie_mem_maxGenEigenspace_toEnd, LieModule.isTrivial_of_nilpotencyLength_le_one, IsSl2Triple.lie_h_e_smul, LieAlgebra.Extension.ringModuleOf_bracket, LieAlgebra.ad_pow_lie, LieModule.Cohomology.d₁₂_apply_coe_apply_apply, LieModule.nilpotencyLength_eq_one_iff, LieHom.lie_apply, LieIdeal.isLieAbelian_iff, LieAlgebra.abelian_iff_derived_one_eq_bot, Derivation.commutator_coe_linear_map, LieDerivation.lie_lieDerivation_apply, LieModule.mem_maxTrivSubmodule, LieModule.Cohomology.d₁₂_apply_apply_ofTrivial, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', FreeLieAlgebra.liftAux_map_mul, LieAlgebra.SpecialLinear.sl_bracket, compLieHom_apply, LieModule.lie_traceForm_eq_zero, neg_lie, LieDerivation.leibniz_lie, LieRing.of_associative_ring_bracket, LieSubmodule.lie_mem, Module.End.lie_apply, LieModule.lie_smul, two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add, lie_zsmul, LieModule.toModuleHom_apply, lie_skew, add_lie, Matrix.lie_apply, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LieDerivation.lie_coe_lieDerivation_apply, smul_lie, LieModule.toEnd_lie, LieAlgebra.ExtendScalars.bracket_tmul, LieSubalgebra.instIsLieTowerSubtypeMem, sum_lie, LieModule.exists_forall_lie_eq_smul, LieRinehartRing.leibniz_smul_right, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, LieSubalgebra.coe_bracket, LieHom.isIdealMorphism_iff, LieModule.shiftedGenWeightSpace.coe_lie_shiftedGenWeightSpace_apply, LieAlgebra.ad_apply, lie_jacobi, LieModule.instIsTrivialOfSubsingleton, IsSl2Triple.HasPrimitiveVectorWith.lie_e, TensorProduct.LieModule.lie_tmul_right, LieAlgebra.Extension.bracket, LieSubmodule.mem_idealizer, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, LieAlgebra.isLieAbelian_iff_center_eq_top, LieDerivation.commutator_coe_linear_map, LieModule.LinearWeights.map_lie, DirectSum.lie_of_same, LieModule.toEnd_pow_lie, LieModule.toEnd_apply_apply, LieSubmodule.lie_mem_lie, Module.Dual.lie_apply, LieModule.smul_lie, RootPairing.GeckConstruction.f_lie_v_ne, LieAlgebra.matrix_trace_commutator_zero, LieSubalgebra.mem_normalizer_iff', LieSubmodule.coe_bracket, LieAlgebra.IsSemisimple.non_abelian_of_isAtom, RootPairing.GeckConstruction.e_lie_v_ne, LieAlgebra.abelian_of_le_center, LieDerivation.SMulBracketCommClass.smul_bracket_comm, LieSubalgebra.exists_lieIdeal_coe_eq_iff, IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, LieModule.isLieAbelian_of_ker_traceForm_eq_bot, LieModule.Weight.apply_lie, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, LieDerivation.lie_ad, Matrix.lie_transpose, lie_add, LieSubmodule.Quotient.mk_bracket, zero_lie, lie_sub, LieDerivation.leibniz', lie_zero, LieModuleHom.map_lie', lie_eq_smul, LieModule.isTrivial_iff_max_triv_eq_top, RootPairing.GeckConstruction.lie_e_lie_f_apply, LieIdeal.isLieAbelian_of_trivial, Submodule.exists_lieSubalgebra_coe_eq_iff, LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace, LieModule.traceForm_apply_lie_apply, LieSubmodule.lieIdeal_oper_eq_linear_span, LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq, LieAlgebra.mem_corootSpace', LieAlgebra.ad_lie, RootPairing.GeckConstruction.f_lie_v_same, LieAlgebra.Extension.ringModuleOf_bracket_proj, IsSl2Triple.lie_h_f_nsmul, LieAlgebra.abelian_derivedAbelianOfIdeal, LieSubmodule.lieIdeal_oper_eq_span, LieAlgebra.abelian_iff_derived_succ_eq_bot, LieHom.map_lie', sum_lie_sum, LieDerivation.apply_lie_eq_sub, IsSl2Triple.lie_h_e_nsmul, LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter, instIsLieTowerSubtypeMemLieSubmodule_1, IsSl2Triple.HasPrimitiveVectorWith.lie_h, LieModuleHom.map_lie, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, LieRinehartAlgebra.Hom.apply_lie', LieAlgebra.mem_corootSpace, lie_nsmul, LieModule.Cohomology.mem_twoCocycle_iff_of_trivial, LieAlgebra.lieCharacter_apply_lie, lie_mem_right, LieAlgebra.lieCharacter_apply_lie', nsmul_lie, LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left, LieModule.traceForm_apply_lie_apply', lie_mem_left, instIsLieTowerSubtypeMemLieSubmodule, LieSubalgebra.lie_mem_sup_of_mem_normalizer, lie_lie, LieAlgebra.IsSimple.non_abelian, LieSubalgebra.lie_mem', LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff, LieDerivation.iterate_apply_lie', LieSubmodule.mem_normalizer, IsSl2Triple.lie_e_f, LieAlgebra.Extension.lie_toKer_apply, sub_lie, LieSubmodule.lie_eq_bot_iff, LieAlgebra.rootSpaceProduct_tmul, leibniz_lie, LieSubalgebra.mem_normalizer_iff, lie_add, TrivialLieModule.instIsTrivial, LieSubmodule.lie_coe_mem_lie, LieModuleHom.map_lie₂, RootPairing.GeckConstruction.e_lie_u, LieRinehartAlgebra.Hom.apply_lie, LieSubalgebra.lie_mem, add_lie, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra, LieDerivation.ad_apply_apply
toEnd 📖	CompOp	1 math math: toEnd_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_lie 📖	mathematical	—	Bracket.bracket toBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup	—	—
compLieHom_apply 📖	mathematical	—	Bracket.bracket toBracket compLieHom DFunLike.coe LieHom LieHom.instFunLike	—	—
leibniz_lie 📖	mathematical	—	Bracket.bracket toBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toBracket	—	—
lie_add 📖	mathematical	—	Bracket.bracket toBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	—
toEnd_apply_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instFunLike LieRing.toAddCommGroup AddMonoidHom.instAddCommGroup toEnd Bracket.bracket toBracket	—	—

LinearMap

Definitions

Name	Category	Theorems
instLieRingModule 📖	CompOp	16 math math: TensorProduct.LieModule.liftLie_apply, BilinForm.isSkewAdjoint_bracket, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom, BilinForm.lieInvariant_iff, LieHom.lie_apply, Derivation.commutator_coe_linear_map, TensorProduct.LieModule.coe_liftLie_eq_lift_coe, instLieModule, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, LieModule.lie_traceForm_eq_zero, LieDerivation.lie_coe_lieDerivation_apply, TensorProduct.LieModule.lift_apply, LieDerivation.commutator_coe_linear_map, LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm, LieModule.coe_maxTrivLinearMapEquivLieModuleHom, LieModuleHom.map_lie₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLieModule 📖	mathematical	—	LieModule LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid addCommGroup module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing instLieRingModule	—	smulCommClass_self ext smul_lie map_smul SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass smul_sub lie_smul

Module.Dual

Definitions

Name	Category	Theorems
instLieRingModule 📖	CompOp	4 math math: LinearMap.BilinForm.lieInvariant_iff, LieModule.lie_traceForm_eq_zero, lie_apply, instLieModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLieModule 📖	mathematical	—	LieModule LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring instLieRingModule	—	smulCommClass_self LinearMap.ext smul_lie map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mul_neg
lie_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike Bracket.bracket LieRingModule.toBracket LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing instLieRingModule NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—

(root)

Definitions

Name	Category	Theorems
IsLieTower 📖	CompData	4 math math: instIsLieTower, LieSubalgebra.instIsLieTowerSubtypeMem, instIsLieTowerSubtypeMemLieSubmodule_1, instIsLieTowerSubtypeMemLieSubmodule
LieAlgebra 📖	CompData	2 math math: instSubsingletonLieAlgebraRat, LieAlgebra.toModule_injective
LieEquiv 📖	CompData	51 math math: skewAdjointMatricesLieSubalgebraEquivTranspose_apply, LieEquiv.map_lie, Matrix.lieConj_apply, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, skewAdjointLieSubalgebraEquiv_apply, LieSubalgebra.equivOfLe_apply, LieEquiv.one_apply, skewAdjointLieSubalgebraEquiv_symm_apply, LieEquiv.coe_injective, LieHom.quotKerEquivRange_toFun, LieHom.equivRangeOfInjective_apply, LieAlgebra.Extension.toKer_bracket, LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, lieEquivMatrix'_apply, LieDerivation.exp_map_apply, LieEquiv.ext_iff, LieAlgebra.Extension.ringModuleOf_bracket, LieEquiv.ofEq_apply, LieEquiv.trans_apply, LieEquiv.ofSubalgebras_apply, Matrix.reindexLieEquiv_apply, LieAlgebra.LieEquiv.ofCoboundary_toFun, LieEquiv.lieSubalgebraMap_apply, AlgEquiv.toLieEquiv_symm_apply, Matrix.lieConj_symm_apply, LieEquiv.apply_symm_apply, LieIdeal.topEquiv_apply, LinearEquiv.lieConj_apply, LieAlgebra.conj_ad_apply, LieEquiv.symm_apply_apply, LieAlgebra.Extension.bracket, RootPairing.GeckConstruction.ωConj_toFun, LieEquiv.symm_bijective, lieEquivMatrix'_symm_apply, LieSubalgebra.topEquiv_apply, LieEquiv.ofSubalgebras_symm_apply, RootPairing.GeckConstruction.ωConj_mem_of_mem, LieEquiv.ofInjective_apply, LieEquiv.toLinearEquiv_injective, LieAlgebra.Extension.ringModuleOf_bracket_proj, LieEquiv.ofBijective_toFun, LieEquiv.coe_coe, skewAdjointMatricesLieSubalgebraEquiv_apply, AlgEquiv.toLieEquiv_apply, LieEquiv.refl_apply, LieAlgebra.Extension.lie_toKer_apply, LieEquiv.coe_toLieHom, LieAlgebra.Extension.oneCochainOfTwoSplitting_apply, LieEquiv.instLinearEquivClass, LieEquiv.coe_toLinearEquiv, LieAlgebra.killingForm_of_equiv_apply
LieHom 📖	CompData	184 math math: LieEquiv.bijective, LieHom.coe_zero, LieAlgebra.Extension.incl_apply_mem_ker, LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, LieDerivation.lie_der_ad_eq_ad_der, LieDerivation.ad_apply_lieDerivation, LieSubalgebra.inclusion_apply, LieHom.ext_iff, LieHom.zero_apply, LieHom.congr_fun, LieModule.toEnd_pow_apply_map, LieEquiv.injective, LieModule.trace_toEnd_eq_zero_of_mem_lcs, LieHom.surjective_rangeRestrict, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LieAlgebra.finrank_engel, LieSubalgebra.equivOfLe_apply, LieHom.mem_idealRange, LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, LieSubalgebra.toEnd_eq, LieDerivation.IsKilling.exists_eq_ad, LieModule.isNilpotent_toEnd_genWeightSpace_zero, LieIdeal.incl_injective, LieHom.coe_id, LieModule.trace_toEnd_genWeightSpace, UniversalEnvelopingAlgebra.lift_unique, LieModule.shiftedGenWeightSpace.toEnd_eq, FreeLieAlgebra.of_comp_lift, LieHom.one_apply, LieSubmodule.Quotient.toEnd_comp_mk', LieModule.mem_posFittingCompOf, LieHom.mem_range_self, LieAlgebra.Extension.toKer_bracket, LieAlgebra.rank_le_natTrailingDegree_charpoly_ad, LieSubmodule.lie_top_eq_of_span_sup_eq_top, LieAlgebra.ad_eq_lmul_left_sub_lmul_right, LieModule.isNilpotent_toEnd_of_isNilpotent, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.coe_map_toEnd_le, LieModule.mem_genWeightSpace, UniversalEnvelopingAlgebra.ι_comp_lift, FreeLieAlgebra.lift_comp_of, LieAlgebra.Extension.incl_injective, LieAlgebra.Extension.lie_incl_mem_ker, LieSubalgebra.toEnd_mk, LieHom.ker_eq_bot, LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, LieModule.coe_genWeightSpaceOf_zero, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, LieHom.map_lie, LieSubmodule.traceForm_eq_zero_of_isTrivial, LieModule.weight_vector_multiplication, LieSubalgebra.coe_ad_pow, LieRinehartAlgebra.Hom.map_smul_apply', RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, LieModule.isFaithful_iff, LieAlgebra.Extension.ringModuleOf_bracket, LieSubalgebra.coe_inclusion, LieSubmodule.toEnd_comp_subtype_mem, LieAlgebra.ad_nilpotent_of_nilpotent, DirectSum.lieAlgebraComponent_apply, LieAlgebra.ad_pow_lie, LieHom.comp_apply, LieModule.isNilpotent_toEnd_of_isNilpotent₂, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, LieHom.toNonUnitalAlgHom_toFun, LieModule.exists_forall_pow_toEnd_eq_zero, DirectSum.lieAlgebraOf_apply, LieDerivation.IsKilling.ad_mem_orthogonal_of_mem_orthogonal, JacobsonNoether.exist_pow_eq_zero_of_le, LieHom.rangeRestrict_apply, LieRingModule.compLieHom_apply, LieSubmodule.toEnd_restrict_eq_toEnd, LieIdeal.coe_inclusion, UniversalEnvelopingAlgebra.lift_ι_apply, LieHom.coe_range, FreeLieAlgebra.lift_unique, LieModule.IsFaithful.injective_toEnd, LieSubalgebra.mem_comap, LieIdeal.inclusion_injective, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply, LieHom.range_eq_top, killingForm_apply_apply, LieSubalgebra.mem_engel_iff, LieModule.iterate_toEnd_mem_lowerCentralSeries₂, LieHom.coe_comp, IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat, LieModule.toEnd_eq_iff, LieHom.id_apply, LieModule.isNilpotent_toEnd_of_mem_rootSpace, UniversalEnvelopingAlgebra.lift_symm_apply, LieHom.range_coe, LieDerivation.toLinearMapLieHom_injective, LieEquiv.surjective, LieModule.toEnd_lie, LieHom.toFun_eq_coe, LieHom.isIdealMorphism_iff, LieAlgebra.ad_apply, LieAlgebra.toEnd_pow_apply_mem, LieHom.instLinearMapClass, LieModule.coe_genWeightSpace_of_top, LieAlgebra.conj_ad_apply, LieAlgebra.Extension.ofTwoCocycle_proj_apply, LieSubalgebra.inclusion_injective, LieHom.coe_mk, LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, UniversalEnvelopingAlgebra.ι_apply, LieHom.coe_toLinearMap, LieModule.toEnd_pow_lie, LieSubmodule.coe_toEnd, LieModule.toEnd_apply_apply, LieAlgebra.Extension.ofTwoCocycle_incl_apply, LieHom.coe_injective, LieModule.commute_toEnd_of_mem_center_right, LieHom.coe_one, LieModule.toEnd_baseChange, FreeLieAlgebra.hom_ext_iff, LieHom.toNonUnitalAlgHom_apply, LieModule.isNilpotent_iff_forall, LieModule.isNilpotent_toEnd_sub_algebraMap, AlgHom.coe_toLieHom, IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, LieDerivation.lie_ad, LieAlgebra.Extension.proj_incl, LieHom.mem_ker, LieSubalgebra.coe_incl, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieModule.toEnd_eq_zero_iff, LieAlgebra.isNilpotent_ad_of_mem_rootSpace, LieModule.traceForm_apply_apply, LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, LieIdeal.mem_comap, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, LieRinehartAlgebra.Hom.map_smul_apply, LieModule.maxGenEigenSpace_toEnd_eq_top, FreeLieAlgebra.lift_symm_apply, LieDerivation.IsKilling.ad_apply_eq_zero_iff, LieSubalgebra.mem_map, LieAlgebra.ad_lie, LieModule.isNilpotent_iff_forall', LieAlgebra.Extension.ringModuleOf_bracket_proj, LieSubmodule.coe_toEnd_pow, LieModule.mem_genWeightSpaceOf, LieDerivation.injective_ad_of_center_eq_bot, LieIdeal.map_le, LieAlgebra.nilpotent_ad_of_nilpotent_algebra, LieAlgebra.Extension.proj_surjective, LieHom.mem_range, FreeLieAlgebra.lift_of_apply, LieAlgebra.mem_zeroRootSubalgebra, LieHom.mem_idealRange_iff, LieRinehartAlgebra.Hom.apply_lie', LieModule.iterate_toEnd_mem_lowerCentralSeries, LieDerivation.coe_ad_apply_eq_ad_apply, LieEquiv.coe_coe, LieAlgebra.isNilpotent_iff_forall, LieDerivation.mem_ad_idealRange_iff, LieHom.le_ker_iff, LieAlgebra.isNilpotent_ad_of_isNilpotent, LieRinehartAlgebra.Hom.toLinearMap'_apply, AlgHom.toLieHom_apply, LieIdeal.incl_apply, LieModule.commute_toEnd_of_mem_center_left, DirectSum.toLieAlgebra_apply, LieAlgebra.Extension.lie_toKer_apply, LieEquiv.coe_toLieHom, LieAlgebra.ExtendScalars.map_apply_tmul, LieHom.range_eq_ker_iff, LieIdeal.inclusion_apply, UniversalEnvelopingAlgebra.lift_ι_apply', LieIdeal.mem_map, LieRinehartAlgebra.Hom.apply_lie, LieModule.Weight.hasEigenvalueAt, LieModule.rank_le_natTrailingDegree_charpoly_ad, LieSubalgebra.coe_ad, LieModule.toEnd_pow_comp_lieHom, LieHom.toNonUnitalAlgHom_injective, LieDerivation.ad_apply_apply, LieSubalgebra.ad_comp_incl_eq
LieModule 📖	CompData	20 math math: LieModule.shiftedGenWeightSpace.instSubtypeMemLieSubmodule, LieModule.ofAssociativeModule, instLieModuleInt, Module.End.instLieModule, TrivialLieModule.instLieModule, lieAlgebraSelfModule, LieIdeal.lieModule, Derivation.instLieModule, LieAlgebra.Extension.lieModuleOf, Matrix.instLieModuleForall, LinearMap.instLieModule, LieSubalgebra.lieModule, LieSubmodule.Quotient.lieQuotientLieModule, LieDerivation.instLieModule, LieAlgebra.ExtendScalars.instLieModule, TensorProduct.LieModule.lieModule, LieSubmodule.instLieModule, Module.Dual.instLieModule, LieRinehartAlgebra.toLieModule, LieModule.compLieHom
LieModuleEquiv 📖	CompData	20 math math: LieModuleEquiv.injective, LieModuleEquiv.refl_apply, LieModuleEquiv.apply_eq_iff_eq_symm_apply, LieModuleEquiv.toEquiv_injective, LieModuleEquiv.symm_apply_apply, TensorProduct.LieModule.coe_liftLie_eq_lift_coe, LieModuleEquiv.trans_apply, LieModuleEquiv.instLinearEquivClass, LieModuleEquiv.coe_toLinearEquiv, TensorProduct.LieModule.lift_apply, LieModuleEquiv.ofTop_apply, LieModuleEquiv.coe_mk, LieModuleEquiv.ext_iff, LieModuleEquiv.symm_bijective, LieModuleEquiv.apply_symm_apply, LieModule.coe_maxTrivEquiv_apply, LieModuleEquiv.coe_toLieModuleHom, LieModuleEquiv.coe_coe, LieModuleEquiv.surjective, LieModuleEquiv.one_apply
LieModuleHom 📖	CompData	63 math math: LieModuleHom.mem_range, TensorProduct.LieModule.liftLie_apply, LieSubmodule.coe_map, LieModule.toEnd_pow_apply_map, LieSubmodule.Quotient.mk_eq_zero, LieModuleHom.zsmul_apply, LieSubmodule.mem_comap, LieModuleHom.ker_eq_bot, LieModuleEquiv.toEquiv_mk, LieModuleHom.coe_mk, LieModuleHom.instLinearMapClass, LieModuleHom.coe_id, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom, LieSubmodule.incl_apply, LieModuleHom.mem_ker, LieModuleHom.coe_toLinearMap, LieModuleHom.comp_apply, LieModuleHom.coe_smul, LieModuleHom.coe_zsmul, LieModuleHom.coe_injective, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieModuleHom.smul_apply, LieModuleHom.nsmul_apply, LieModuleHom.coe_neg, TensorProduct.LieModule.map_tmul, LieModuleHom.coe_restrictLie, LieSubalgebra.coe_incl', TensorProduct.LieModule.coe_liftLie_eq_lift_coe, LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, LieModuleHom.coe_range, LieSubmodule.coe_inclusion, LieModuleHom.comp_ker_incl, LieModule.toModuleHom_apply, LieModuleHom.zero_apply, LieModuleHom.neg_apply, LieModuleHom.range_eq_top, LieModuleHom.coe_add, LieSubmodule.Quotient.surjective_mk', LieModuleHom.coe_comp, LieModuleEquiv.coe_mk, LieSubmodule.incl_eq_val, LieModuleHom.coe_nsmul, LieSubmodule.inclusion_apply, LieModuleHom.id_apply, LieModuleHom.coe_zero, LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm, LieModuleHom.add_apply, LieSubmodule.mem_map_of_mem, LieSubmodule.inclusion_injective, LieModuleHom.map_lie, LieModuleEquiv.coe_toLieModuleHom, LieModuleHom.coe_sub, LieModule.coe_maxTrivHom_apply, LieModuleHom.sub_apply, LieModuleHom.ext_iff, LieModuleEquiv.coe_coe, LieModuleHom.congr_fun, LieSubmodule.Quotient.mk'_apply, LieSubmodule.injective_incl, LieAlgebra.rootSpaceProduct_tmul, LieModule.coe_maxTrivLinearMapEquivLieModuleHom, LieSubmodule.mem_map, LieModuleHom.map_lie₂
LieRing 📖	CompData	—
LieRingModule 📖	CompData	—
lieRingSelfModule 📖	CompOp	340 math math: LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map, LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieAlgebra.Extension.incl_apply_mem_ker, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, LieDerivation.lie_der_ad_eq_ad_der, LieDerivation.instNoetherian, DirectSum.bracket_apply, LieDerivation.ad_apply_lieDerivation, LieDerivation.iterate_apply_lie, LieIdeal.map_bracket_le, Function.Surjective.isLieAbelian, LieDerivation.IsKilling.instIsKilling_range_ad, LieAlgebra.abelian_radical_of_hasTrivialRadical, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, LieIdeal.comap_incl_eq_top, LieAlgebra.derivedLength_zero, LieSubalgebra.isLieAbelian_lieSpan_iff, LieIdeal.restrict_killingForm, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, LieEquiv.map_lie, LieIdeal.coe_bracket_of_module, Matrix.isSkewAdjoint_bracket, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, LieAlgebra.isSolvable_iff_int, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, LieModule.derivedSeries_le_lowerCentralSeries, LieHom.mem_idealRange, LieSubmodule.bot_lie, LieIdeal.gc_map_comap, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieIdeal.map_comap_incl, LieDerivation.IsKilling.exists_eq_ad, LieAlgebra.coe_zeroRootSubalgebra, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, LieAlgebra.hasTrivialRadical_iff, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, LieIdeal.incl_injective, LieDerivation.apply_lie_eq_add, LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap, IsSl2Triple.lie_lie_smul_f, LieAlgebra.IsSemisimple.booleanGenerators, LieAlgebra.derivedSeriesOfIdeal_succ_le, LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra, LieSubmodule.lieIdeal_oper_eq_linear_span', LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall, LieDerivation.commutator_apply, LieHom.quotKerEquivRange_toFun, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieIdeal.lowerCentralSeries_map_eq, LieAlgebra.derivedSeries_of_derivedLength_succ, LieModule.Cohomology.d₂₃_apply, LieIdeal.coe_killingCompl_top, LieModule.Cohomology.d₁₂_apply_apply, LieAlgebra.Extension.toKer_bracket, LieAlgebra.non_trivial_center_of_isNilpotent, DirectSum.lie_of_of_ne, LieAlgebra.bracket_ofTwoCocycle, LieIdeal.instIsNilpotentSubtypeMemLieSubmoduleOfIsNilpotent, LieIdeal.coe_toLieSubalgebra, LieSubmodule.lie_top_eq_of_span_sup_eq_top, DirectSum.lie_of, LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff, LieIdeal.mem_killingCompl, LieAlgebra.abelian_radical_iff_solvable_is_abelian, two_nsmul_lie_lmul_lmul_add_add_eq_zero, LieModule.instIsTriangularizableSubtypeMemLieSubmodule, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.sup_lie, commutative_ring_iff_abelian_lie_ring, LieModule.mem_ker, lie_abelian_iff_equiv_lie_abelian, LieRing.lie_apply, LieIdeal.le_killingCompl_top_of_isLieAbelian, LieAlgebra.IsKilling.chainLength_zero, LieAlgebra.self_module_ker_eq_center, lieAlgebraSelfModule, LieIdeal.incl_coe, LieSubalgebra.ideal_in_normalizer, LieAlgebra.Extension.lie_incl_mem_ker, LieAlgebra.radical_eq_top_of_isSolvable, LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, LieIdeal.derivedSeries_map_le, LieHom.ker_eq_bot, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', IsSl2Triple.mem_toLieSubalgebra_iff, LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff, LieIdeal.incl_isIdealMorphism, LieSubalgebra.coe_normalizer_eq_normalizer, LieAlgebra.rootSpaceProduct_def, LieHom.map_lie, LieModule.instLinearWeightsOfIsLieAbelian, LieModule.lowerCentralSeries_succ, LieSubmodule.lie_le_inf, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, LieAlgebra.derivedSeriesOfIdeal_le_self, LieIdeal.lieModule, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, Function.Injective.isLieAbelian, LieIdeal.subsingleton_of_bot, LieAlgebra.isSolvable_iff, LieSubalgebra.mem_toLieSubmodule, LieIdeal.toLieSubalgebra_toSubmodule, LieAlgebra.derivedSeriesOfIdeal_succ, LieDerivation.IsKilling.killingForm_restrict_range_ad, IsSl2Triple.lie_h_e_smul, LieAlgebra.Extension.ringModuleOf_bracket, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, LieAlgebra.IsKilling.chainLength_neg, LieAlgebra.IsSimple.isAtom_top, LieAlgebra.ad_pow_lie, LieModule.Cohomology.d₁₂_apply_coe_apply_apply, LieIdeal.isLieAbelian_iff, LieAlgebra.instIsFaithfulOfHasTrivialRadical, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieAlgebra.abelian_iff_derived_one_eq_bot, LieIdeal.incl_range, LieIdeal.map_mono, LieAlgebra.IsKilling.apply_coroot_eq_cast, LieSubalgebra.coe_incl', LieModule.Cohomology.d₁₂_apply_apply_ofTrivial, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', FreeLieAlgebra.liftAux_map_mul, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieSubmodule.lie_comm, LieAlgebra.center_le_radical, LieAlgebra.SpecialLinear.sl_bracket, coe_lowerCentralSeries_ideal_quot_eq, LieModule.Weight.isZero_neg, LieHom.ker_le_comap, LieAlgebra.zero_rootSpace_eq_top_of_nilpotent, LieModule.lie_traceForm_eq_zero, LieDerivation.leibniz_lie, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, LieRing.of_associative_ring_bracket, LieIdeal.comap_bracket_le, LieDerivation.lie_apply, LieIdeal.map_lowerCentralSeries_le, LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra, LieAlgebra.hasTrivialRadical_iff_no_solvable_ideals, two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add, LieIdeal.map_sup_ker_eq_map', LieAlgebra.derivedSeriesOfIdeal_antitone, LieSubmodule.lie_baseChange, LieModule.toModuleHom_apply, LieAlgebra.IsExtension.ker_eq_bot, LieSubmodule.top_lie_le_iff_le_normalizer, LieIdeal.topEquiv_apply, lie_skew, LieAlgebra.IsSolvable.solvable_int, LieAlgebra.derivedSeries_baseChange, LieAlgebra.derivedSeriesOfIdeal_add_le_add, LieDerivation.toLinearMapLieHom_injective, LieDerivation.ad_isIdealMorphism, LieAlgebra.derivedSeries_def, LieIdeal.coe_map_of_surjective, LieDerivation.lie_coe_lieDerivation_apply, LieSubalgebra.instIsLieTowerSubtypeMem, LieRinehartRing.leibniz_smul_right, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieSubalgebra.coe_bracket, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieHom.isIdealMorphism_iff, LieAlgebra.ad_apply, LieIdeal.isCompl_killingCompl, lie_jacobi, LieDerivation.IsKilling.rangeAdOrthogonal_carrier, LieHom.quotKerEquivRange_invFun, LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal, LieIdeal.derivedSeries_eq_bot_iff, LieAlgebra.Extension.bracket, LieIdeal.comap_bracket_incl, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, LieSubmodule.mem_idealizer, LieIdeal.killingForm_eq, LieAlgebra.center_eq_bot, LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit, LieAlgebra.rootSpace_comap_eq_genWeightSpace, LieModule.isFaithful_iff_ker_eq_bot, LieAlgebra.isLieAbelian_iff_center_eq_top, LieDerivation.commutator_coe_linear_map, LieModule.LinearWeights.map_lie, DirectSum.lie_of_same, LieAlgebra.restrict_killingForm, LieIdeal.coe_derivedSeries_eq_int, LieIdeal.map_comap_bracket_eq, LieHom.idealRange_eq_map, LieModule.le_max_triv_iff_bracket_eq_bot, LieSubalgebra.coe_toLieSubmodule, LieAlgebra.IsKilling.coroot_neg, LieAlgebra.matrix_trace_commutator_zero, LieSubalgebra.mem_normalizer_iff', LieAlgebra.maxNilpotentIdeal_eq_top_of_isNilpotent, LieHom.idealRange_eq_lieSpan_range, LieIdeal.comap_mono, LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, LieIdeal.incl_idealRange, LieSubmodule.inf_lie, LieAlgebra.HasTrivialRadical.radical_eq_bot, LieSubalgebra.exists_lieIdeal_coe_eq_iff, LieIdeal.comap_incl_self, LieDerivation.IsKilling.range_ad_eq_top, LieModule.isLieAbelian_of_ker_traceForm_eq_bot, LieModule.Weight.apply_lie, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieDerivation.lie_ad, LieAlgebra.IsSimple.instIsIrreducible, LieHom.mem_ker, LieSubalgebra.normalizer_eq_self_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, Matrix.lie_transpose, LieSubmodule.Quotient.mk_bracket, LieAlgebra.IsKilling.killingCompl_top_eq_bot, LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieDerivation.leibniz', LieIdeal.map_comap_eq, LieIdeal.comap_map_le, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals, LieAlgebra.isFaithful_self_iff, LieHom.range_subset_idealRange, LieAlgebra.radicalIsSolvable, LieIdeal.mem_comap, LieIdeal.map_bracket_eq, LieSubmodule.lieIdeal_oper_eq_tensor_map_range, LieIdeal.map_le_iff_le_comap, LieIdeal.isLieAbelian_of_trivial, LieIdeal.top_toLieSubalgebra, Submodule.exists_lieSubalgebra_coe_eq_iff, LieModule.traceForm_apply_lie_apply, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieSubmodule.lieIdeal_oper_eq_linear_span, LieDerivation.IsKilling.ad_apply_eq_zero_iff, LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq, LieAlgebra.mem_corootSpace', LieAlgebra.derivedSeries_lt_top_of_solvable, LieIdeal.derivedSeries_succ_eq_top_iff, LieAlgebra.ad_lie, LieAlgebra.derivedSeries_of_bot_eq_bot, LieAlgebra.Extension.ringModuleOf_bracket_proj, IsSl2Triple.lie_h_f_nsmul, LieAlgebra.abelian_derivedAbelianOfIdeal, LieHom.map_le_idealRange, LieSubmodule.lieIdeal_oper_eq_span, LieAlgebra.abelian_iff_derived_succ_eq_bot, LieHom.map_lie', LieDerivation.apply_lie_eq_sub, LieAlgebra.IsKilling.traceForm_coroot, LieIdeal.map_le, IsSl2Triple.lie_h_e_nsmul, LieAlgebra.toLieSubmodule_le_rootSpace_zero, LieAlgebra.IsKilling.coroot_zero, LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter, instIsLieTowerSubtypeMemLieSubmodule_1, LieModule.Weight.isNonZero_neg, LieAlgebra.derivedSeriesOfIdeal_baseChange, LieSubmodule.exists_smul_add_of_span_sup_eq_top, LieAlgebra.center_le_maxNilpotentIdeal, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieSubmodule.lcs_succ, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, LieHom.mem_idealRange_iff, LieAlgebra.mem_corootSpace, LieModule.Cohomology.mem_twoCocycle_iff_of_trivial, LieAlgebra.isSolvableAdd, LieIdeal.toSubmodule_killingCompl, LieAlgebra.maxNilpotentIdeal_le_radical, LieAlgebra.lieCharacter_apply_lie, LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable, LieHom.ker_toSubmodule, LieAlgebra.maxNilpotentIdealIsNilpotent, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieIdeal.coe_lcs_eq, LieDerivation.coe_ad_apply_eq_ad_apply, LieAlgebra.lieCharacter_apply_lie', LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical, LieAlgebra.IsKilling.span_weight_eq_top, LieDerivation.ad_ker_eq_center, LieModule.traceForm_apply_lie_apply', LieDerivation.mem_ad_idealRange_iff, LieAlgebra.derivedLength_eq_derivedLengthOfIdeal, LieHom.le_ker_iff, LieAlgebra.IsSemisimple.sSupIndep_isAtom, instIsLieTowerSubtypeMemLieSubmodule, LieModule.Weight.toLinear_neg, LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, LieSubalgebra.lie_mem_sup_of_mem_normalizer, LieAlgebra.Extension.twoCocycleOf_coe_coe, LieAlgebra.isSolvableBot, LieIdeal.comap_bracket_eq, LieAlgebra.LieIdeal.solvable_iff_le_radical, lie_lie, LieIdeal.incl_apply, LieAlgebra.IsSolvable.solvable, Function.instIsSolvableSubtypeMemLieSubmodule, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.IsSimple.non_abelian, LieSubalgebra.lie_mem', LieDerivation.iterate_apply_lie', LieAlgebra.ad_ker_eq_self_module_ker, LieIdeal.map_sup_ker_eq_map, IsSl2Triple.lie_e_f, LieAlgebra.IsSimple.isAtom_iff_eq_top, LieAlgebra.Extension.lie_toKer_apply, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieAlgebra.rootSpaceProduct_tmul, LieModule.traceForm_lieInvariant, LieSubalgebra.mem_normalizer_iff, LieIdeal.ker_incl, LieSubmodule.lie_le_left, LieIdeal.lcs_top, LieAlgebra.IsKilling.rootSystem_root_apply, LieIdeal.comap_incl_eq_bot, LieIdeal.map_eq_bot_iff, LieSubalgebra.normalizer_eq_self_of_isCartanSubalgebra, LieSubmodule.lie_coe_mem_lie, LieModule.coe_lowerCentralSeries_ideal_le, LieModule.Weight.coe_neg, LieAlgebra.Extension.oneCochainOfTwoSplitting_apply, LieIdeal.comap_toSubmodule, LieIdeal.map_comap_le, LieAlgebra.isExtension_of_surjective, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, LieIdeal.idealizer_eq_normalizer, LieAlgebra.IsSimple.eq_bot_or_eq_top, LieModule.ker_eq_bot, LieIdeal.map_sup, LieSubalgebra.lie_mem, LieHom.idealRange_eq_top_of_surjective, LieSubmodule.gc_top_lie_normalizer, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra, LieDerivation.ad_apply_apply
«term_→ₗ⁅_,_⁆_» 📖	CompOp	—
«term_→ₗ⁅_⁆_» 📖	CompOp	—
«term_≃ₗ⁅_,_⁆_» 📖	CompOp	—
«term_≃ₗ⁅_⁆_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup	—	LieRingModule.add_lie
instIsLieTower 📖	mathematical	—	IsLieTower LieRing.toBracket LieRingModule.toBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	LieRingModule.leibniz_lie
instLieModuleInt 📖	mathematical	—	LieModule Int.instCommRing LieRing.instLieAlgebra AddCommGroup.toIntModule	—	zsmul_lie lie_zsmul
instSubsingletonLieAlgebraRat 📖	mathematical	—	LieAlgebra Rat.commRing	—	Function.Injective.subsingleton LieAlgebra.toModule_injective subsingleton_rat_module
leibniz_lie 📖	mathematical	—	Bracket.bracket	—	IsLieTower.leibniz_lie
lieAlgebraSelfModule 📖	mathematical	—	LieModule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	lie_skew LieAlgebra.lie_smul smul_neg
lie_add 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	LieRingModule.lie_add
lie_jacobi 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup Bracket.bracket LieRingModule.toBracket lieRingSelfModule NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_neg lie_neg lie_skew lie_lie Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add add_zero Mathlib.Tactic.Abel.zero_termg
lie_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	leibniz_lie instIsLieTower add_sub_cancel_right
lie_neg 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	sub_eq_zero sub_neg_eq_add lie_add neg_add_cancel lie_zero
lie_nsmul 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	AddMonoidHom.map_nsmul lie_zero lie_add
lie_self 📖	mathematical	—	Bracket.bracket LieRing.toBracket NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	LieRing.lie_self
lie_skew 📖	mathematical	—	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup Bracket.bracket LieRingModule.toBracket lieRingSelfModule	—	lie_add lie_self add_lie zero_add add_zero
lie_smul 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket 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 AddCommGroup.toAddCommMonoid	—	LieModule.lie_smul
lie_sub 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_eq_add_neg lie_add lie_neg
lie_sum 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket Finset.sum AddCommGroup.toAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
lie_swap_lie 📖	mathematical	—	Bracket.bracket NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	leibniz_lie add_sub_cancel_right sub_add_cancel_right
lie_zero 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	AddMonoidHom.map_zero lie_add
lie_zsmul 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	AddMonoidHom.map_zsmul lie_zero lie_add
neg_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	sub_eq_zero sub_neg_eq_add add_lie neg_add_cancel zero_lie
nsmul_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup	—	AddMonoidHom.map_nsmul zero_lie add_lie
smul_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket 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	—	LieModule.smul_lie
sub_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup	—	sub_eq_add_neg add_lie neg_lie
sum_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket Finset.sum AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup	—	map_sum AddMonoidHom.instAddMonoidHomClass
sum_lie_sum 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket Finset.sum AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup	—	sum_lie Finset.sum_congr lie_sum
zero_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	AddMonoidHom.map_zero add_lie
zsmul_lie 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LieRing.toAddCommGroup	—	AddMonoidHom.map_zsmul zero_lie add_lie

---

← Back to Index