OfAssociative

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

Statistics

Metric	Count
Definitions toLieEquiv, instCoeLieHom, toLieHom, ad, ofAssociativeAlgebra, IsFaithful, toEnd, ofAssociativeRing, ofAssociativeModule, lieConj, instLieRingModule, lieSubalgebraOfSubalgebra	12
Theorems toLieEquiv_apply, toLieEquiv_symm_apply, coe_toLieHom, toLieHom_apply, toLieHom_comp, toLieHom_id, toLieHom_injective, ad_apply, ad_eq_lmul_left_sub_lmul_right, ad_lie, ad_pow_lie, conj_ad_apply, injective_toEnd, ext_of_isFaithful, instIsFaithfulEnd, instIsFaithfulSubtypeMemLieSubalgebra, isFaithful_iff, isFaithful_iff', ofAssociativeModule, toEnd_apply_apply, toEnd_eq_iff, toEnd_eq_zero_iff, toEnd_lie, toEnd_module_end, toEnd_pow_apply_map, toEnd_pow_comp_lieHom, toEnd_pow_lie, lie_apply, of_associative_ring_bracket, ad_comp_incl_eq, coe_ad, coe_ad_pow, toEnd_eq, toEnd_mk, coe_map_toEnd_le, coe_toEnd, coe_toEnd_pow, mapsTo_pow_toEnd_sub_algebraMap, toEnd_comp_subtype_mem, toEnd_restrict_eq_toEnd, lieConj_apply, lieConj_symm, instLieModule, lie_apply, lie_eq_smul	45
Total	57

AlgEquiv

Definitions

Name	Category	Theorems
toLieEquiv 📖	CompOp	2 math math: toLieEquiv_symm_apply, toLieEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLieEquiv_apply 📖	mathematical	—	DFunLike.coe LieEquiv LieRing.ofAssociativeRing LieAlgebra.ofAssociativeAlgebra EquivLike.toFunLike LieEquiv.instEquivLike toLieEquiv AlgEquiv CommRing.toCommSemiring Ring.toSemiring instFunLike	—	—
toLieEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LieEquiv LieRing.ofAssociativeRing LieAlgebra.ofAssociativeAlgebra EquivLike.toFunLike LieEquiv.instEquivLike LieEquiv.symm toLieEquiv AlgEquiv CommRing.toCommSemiring Ring.toSemiring instFunLike symm	—	—

AlgHom

Definitions

Name	Category	Theorems
instCoeLieHom 📖	CompOp	—
toLieHom 📖	CompOp	6 math math: toLieHom_id, UniversalEnvelopingAlgebra.lift_symm_apply, coe_toLieHom, toLieHom_comp, UniversalEnvelopingAlgebra.hom_ext_iff, toLieHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toLieHom 📖	mathematical	—	DFunLike.coe LieHom LieRing.ofAssociativeRing LieAlgebra.ofAssociativeAlgebra LieHom.instFunLike toLieHom AlgHom CommRing.toCommSemiring Ring.toSemiring funLike	—	—
toLieHom_apply 📖	mathematical	—	DFunLike.coe LieHom LieRing.ofAssociativeRing LieAlgebra.ofAssociativeAlgebra LieHom.instFunLike toLieHom AlgHom CommRing.toCommSemiring Ring.toSemiring funLike	—	—
toLieHom_comp 📖	mathematical	—	toLieHom comp CommRing.toCommSemiring Ring.toSemiring LieHom.comp LieRing.ofAssociativeRing LieAlgebra.ofAssociativeAlgebra	—	—
toLieHom_id 📖	mathematical	—	toLieHom id CommRing.toCommSemiring Ring.toSemiring LieHom.id LieRing.ofAssociativeRing LieAlgebra.ofAssociativeAlgebra	—	—
toLieHom_injective 📖	—	toLieHom	—	—	ext LieHom.congr_fun

LieAlgebra

Definitions

Name	Category	Theorems
ad 📖	CompOp	27 math math: finrank_engel, isRegular_iff_natTrailingDegree_charpoly_eq_rank, rank_le_natTrailingDegree_charpoly_ad, ad_eq_lmul_left_sub_lmul_right, LieSubalgebra.coe_ad_pow, ad_nilpotent_of_nilpotent, ad_pow_lie, JacobsonNoether.exist_pow_eq_zero_of_le, killingForm_apply_apply, LieSubalgebra.mem_engel_iff, LieModule.toEnd_lie, ad_apply, conj_ad_apply, LieModule.toEnd_pow_lie, isNilpotent_ad_of_mem_rootSpace, IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, rank_eq_natTrailingDegree, ad_lie, isNilpotent_range_ad_iff, nilpotent_ad_of_nilpotent_algebra, LieDerivation.coe_ad_apply_eq_ad_apply, isNilpotent_iff_forall, ad_ker_eq_bot_of_hasTrivialRadical, isNilpotent_ad_of_isNilpotent, ad_ker_eq_self_module_ker, LieSubalgebra.coe_ad, LieSubalgebra.ad_comp_incl_eq
ofAssociativeAlgebra 📖	CompOp	223 math math: IsKilling.rootSystem_toLinearMap_apply, LinearMap.BilinForm.isSkewAdjoint_bracket, IsKilling.restrict_killingForm_eq_sum, LieSubmodule.lowerCentralSeries_tensor_eq_baseChange, LieModule.toEnd_pow_apply_map, skewAdjointMatricesLieSubalgebraEquivTranspose_apply, RootPairing.GeckConstruction.instHasTrivialRadical, Orthogonal.mem_so, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, LieModule.trace_toEnd_eq_zero_of_mem_lcs, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, Matrix.lieConj_apply, LoopAlgebra.twoCochainOfBilinear_apply_apply, Orthogonal.soIndefiniteEquiv_apply, mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, finrank_engel, skewAdjointLieSubalgebraEquiv_apply, LieModule.traceForm_eq_sum_finrank_nsmul', IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, IsKilling.rootSystem_coroot_apply, isRegular_iff_natTrailingDegree_charpoly_eq_rank, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, LeftInvariantDerivation.left_invariant, LieModule.instIsFaithfulMatrixForall, LieSubalgebra.toEnd_eq, lieCharacterEquivLinearDual_apply, LieModule.isNilpotent_toEnd_genWeightSpace_zero, LieModule.ofAssociativeModule, skewAdjointLieSubalgebraEquiv_symm_apply, LieModule.trace_toEnd_genWeightSpace, AlgHom.toLieHom_id, UniversalEnvelopingAlgebra.lift_unique, LieModule.shiftedGenWeightSpace.toEnd_eq, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, Module.End.instLieModule, LieRinehartAlgebra.Hom.anchor_derivation, LieSubmodule.Quotient.toEnd_comp_mk', LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieModule.mem_posFittingCompOf, SpecialLinear.singleSubSingle_add_singleSubSingle, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, LieModule.isNilpotent_range_toEnd_iff, rank_le_natTrailingDegree_charpoly_ad, LieSubmodule.lie_top_eq_of_span_sup_eq_top, Derivation.bracket_eq_fun, Orthogonal.indefiniteDiagonal_assoc, ad_eq_lmul_left_sub_lmul_right, LieModule.isNilpotent_toEnd_of_isNilpotent, hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.coe_map_toEnd_le, LieModule.mem_genWeightSpace, LoopAlgebra.toFinsupp_symm_single, UniversalEnvelopingAlgebra.ι_comp_lift, LieModule.Weight.coe_coe, LieSubalgebra.toEnd_mk, IsKilling.invtSubmoduleToLieIdeal_top, IsKilling.coe_corootSpace_eq_span_singleton', LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, LeftInvariantDerivation.evalAt_coe, LieModule.coe_genWeightSpaceOf_zero, engel_isBot_of_isMin.lieCharpoly_map_eval, LieSubmodule.traceForm_eq_zero_of_isTrivial, lieEquivMatrix'_apply, LieModule.weight_vector_multiplication, LieSubalgebra.coe_ad_pow, Derivation.instLieModule, IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, lieCharacterEquivLinearDual_symm_apply, instIsSolvableTensorProduct, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LinearMap.BilinForm.lieInvariant_iff, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, Matrix.instLieModuleForall, LieModule.isFaithful_iff, LieSubmodule.toEnd_comp_subtype_mem, ad_nilpotent_of_nilpotent, LieModule.rank_eq_natTrailingDegree, LieSubmodule.mem_baseChange_iff, ad_pow_lie, LieModule.isNilpotent_toEnd_of_isNilpotent₂, RootPairing.GeckConstruction.span_range_h'_eq_top, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, LieModule.Weight.coe_toLinear_eq_zero_iff, Derivation.commutator_coe_linear_map, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieModule.exists_forall_pow_toEnd_eq_zero, IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, JacobsonNoether.exist_pow_eq_zero_of_le, Matrix.reindexLieEquiv_apply, SpecialLinear.sl_bracket, LieSubmodule.toEnd_restrict_eq_toEnd, Matrix.reindexLieEquiv_symm, UniversalEnvelopingAlgebra.lift_ι_apply, LieModule.IsFaithful.injective_toEnd, RootPairing.GeckConstruction.span_range_h_le_range_diagonal, LieModule.instIsNilpotentTensor, AlgEquiv.toLieEquiv_symm_apply, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply, mem_skewAdjointMatricesLieSubalgebra, IsKilling.corootForm_rootSystem_eq_killing, Matrix.lieConj_symm_apply, LieModule.trace_comp_toEnd_genWeightSpace_eq, RootPairing.GeckConstruction.instIsIrreducible, killingForm_apply_apply, LieSubalgebra.mem_engel_iff, LieModule.iterate_toEnd_mem_lowerCentralSeries₂, LieSubmodule.lie_baseChange, IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat, LieModule.toEnd_eq_iff, LinearEquiv.lieConj_apply, LieModule.isNilpotent_toEnd_of_mem_rootSpace, UniversalEnvelopingAlgebra.lift_symm_apply, derivedSeries_baseChange, LieDerivation.toLinearMapLieHom_injective, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LieModule.toEnd_lie, ExtendScalars.bracket_tmul, IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, LoopAlgebra.toFinsupp_single_tmul, ad_apply, toEnd_pow_apply_mem, lieCharacter_apply_of_mem_derived, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, LieModule.traceForm_eq_sum_finrank_nsmul, conj_ad_apply, LieSubmodule.tmul_mem_baseChange_of_mem, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, IsKilling.span_weight_isNonZero_eq_top, RootPairing.GeckConstruction.ωConj_invFun, LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, LieDerivation.commutator_coe_linear_map, UniversalEnvelopingAlgebra.ι_apply, LieModule.toEnd_pow_lie, LieSubmodule.coe_toEnd, LieModule.toEnd_apply_apply, mem_skewAdjointMatricesLieSubalgebra_unit_smul, LieModule.commute_toEnd_of_mem_center_right, LieModule.toEnd_baseChange, RootPairing.GeckConstruction.ωConj_toFun, SpecialLinear.val_single, LieModule.isNilpotent_iff_forall, LieModule.isNilpotent_toEnd_sub_algebraMap, LoopAlgebra.residuePairing_apply_apply, lieEquivMatrix'_symm_apply, SpecialLinear.singleSubSingle_sub_singleSubSingle, RootPairing.GeckConstruction.h_mem_lieAlgebra, AlgHom.coe_toLieHom, IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, IsKilling.rootSystem_pairing_apply, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, IsKilling.cartanEquivDual_apply_apply, LieModule.toEnd_eq_zero_iff, isNilpotent_ad_of_mem_rootSpace, AlgHom.toLieHom_comp, LieModule.traceForm_apply_apply, IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, LieModule.maxGenEigenSpace_toEnd_eq_top, LinearEquiv.lieConj_symm, rank_eq_natTrailingDegree, ad_lie, LieModule.isNilpotent_iff_forall', LeftInvariantDerivation.evalAt_mul, LieSubmodule.coe_toEnd_pow, isNilpotent_range_ad_iff, LieModule.mem_genWeightSpaceOf, IsKilling.traceForm_coroot, UniversalEnvelopingAlgebra.hom_ext_iff, nilpotent_ad_of_nilpotent_algebra, Derivation.commutator_apply, LieModule.instIsFaithfulEnd, derivedSeriesOfIdeal_baseChange, LieModule.coe_lcs_range_toEnd_eq, LieModule.toEnd_module_end, mem_zeroRootSubalgebra, ExtendScalars.instLieModule, LieModule.iterate_toEnd_mem_lowerCentralSeries, isSolvable_tensorProduct_iff, RootPairing.GeckConstruction.f_mem_lieAlgebra, lieCharacter_apply_lie, LieRinehartAlgebra.instDerivation, LieDerivation.coe_ad_apply_eq_ad_apply, lieCharacter_apply_lie', RootPairing.GeckConstruction.e_mem_lieAlgebra, SpecialLinear.val_singleSubSingle, isNilpotent_iff_forall, ad_ker_eq_bot_of_hasTrivialRadical, IsKilling.span_weight_eq_top, skewAdjointMatricesLieSubalgebraEquiv_apply, LoopAlgebra.twoCocycleOfBilinear_coe, LieModule.Weight.toLinear_neg, LieSubmodule.coe_baseChange, Extension.twoCocycleOf_coe_coe, AlgEquiv.toLieEquiv_apply, AlgHom.toLieHom_apply, LieSubmodule.baseChange_top, LieModule.commute_toEnd_of_mem_center_left, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, ad_ker_eq_self_module_ker, LieModule.range_traceForm_le_span_weight, ExtendScalars.map_apply_tmul, LieRinehartAlgebra.toLieModule, SpecialLinear.singleSubSingle_sub_singleSubSingle', IsKilling.rootSystem_root_apply, UniversalEnvelopingAlgebra.lift_ι_apply', LieModule.Weight.instLinearMapClass, LieModule.Weight.hasEigenvalueAt, LieRinehartAlgebra.instLieRinehartRingDerivation, LieModule.rank_le_natTrailingDegree_charpoly_ad, LieSubalgebra.coe_ad, LieModule.toEnd_matrix, LieModule.Weight.toLinear_apply, IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, LieModule.toEnd_pow_comp_lieHom, SpecialLinear.sl_non_abelian, LieSubmodule.baseChange_bot, LeftInvariantDerivation.evalAt_apply, LieSubalgebra.ad_comp_incl_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ad_apply 📖	mathematical	—	DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup toModule LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LieHom LieRing.ofAssociativeRing Module.End.instRing ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike ad Bracket.bracket LieRingModule.toBracket lieRingSelfModule	—	smulCommClass_self IsScalarTower.left
ad_eq_lmul_left_sub_lmul_right 📖	mathematical	—	DFunLike.coe LieHom Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing toModule ofAssociativeAlgebra Module.End.instRing Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike ad Pi.instSub LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instSub LinearMap.mulLeft Algebra.to_smulCommClass LinearMap.mulRight IsScalarTower.right	—	smulCommClass_self IsScalarTower.left Algebra.to_smulCommClass IsScalarTower.right LinearMap.ext
ad_lie 📖	mathematical	—	DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup toModule LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LieHom LieRing.ofAssociativeRing Module.End.instRing ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike ad Bracket.bracket LieRingModule.toBracket lieRingSelfModule AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	LieModule.toEnd_lie lieAlgebraSelfModule
ad_pow_lie 📖	mathematical	—	DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup toModule LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LieHom LieRing.ofAssociativeRing Module.End.instRing ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike ad Bracket.bracket LieRingModule.toBracket lieRingSelfModule Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Nat.choose	—	LieModule.toEnd_pow_lie lieAlgebraSelfModule
conj_ad_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.End AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.conj LieEquiv.toLinearEquiv LieHom LieRing.ofAssociativeRing Module.End.instRing ofAssociativeAlgebra Module.End.instAlgebra CommRing.toCommMonoid Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike ad LieEquiv LieEquiv.instEquivLike	—	LinearMap.ext RingHomInvPair.ids smulCommClass_self IsScalarTower.left LinearEquiv.conj_apply_apply ad_apply LieEquiv.coe_toLinearEquiv LieEquiv.map_lie LinearEquiv.apply_symm_apply

LieModule

Definitions

Name	Category	Theorems
IsFaithful 📖	CompData	8 math math: instIsFaithfulMatrixForall, isFaithful_iff, LieAlgebra.instIsFaithfulOfHasTrivialRadical, isFaithful_iff', isFaithful_iff_ker_eq_bot, LieAlgebra.isFaithful_self_iff, instIsFaithfulEnd, instIsFaithfulSubtypeMemLieSubalgebra
toEnd 📖	CompOp	68 math math: toEnd_pow_apply_map, trace_toEnd_eq_zero_of_mem_lcs, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, exists_genWeightSpace_zero_le_ker_of_isNoetherian, LieSubalgebra.toEnd_eq, isNilpotent_toEnd_genWeightSpace_zero, trace_toEnd_genWeightSpace, shiftedGenWeightSpace.toEnd_eq, LieSubmodule.Quotient.toEnd_comp_mk', instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, mem_posFittingCompOf, isNilpotent_range_toEnd_iff, LieSubmodule.lie_top_eq_of_span_sup_eq_top, isNilpotent_toEnd_of_isNilpotent, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.coe_map_toEnd_le, mem_genWeightSpace, LieSubalgebra.toEnd_mk, exists_genWeightSpace_le_ker_of_isNoetherian, coe_genWeightSpaceOf_zero, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, LieSubmodule.traceForm_eq_zero_of_isTrivial, weight_vector_multiplication, RootPairing.GeckConstruction.trace_toEnd_eq_zero, IsTriangularizable.maxGenEigenspace_eq_top, isFaithful_iff, LieSubmodule.toEnd_comp_subtype_mem, rank_eq_natTrailingDegree, isNilpotent_toEnd_of_isNilpotent₂, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, exists_forall_pow_toEnd_eq_zero, LieSubmodule.toEnd_restrict_eq_toEnd, IsFaithful.injective_toEnd, trace_comp_toEnd_genWeightSpace_eq, iterate_toEnd_mem_lowerCentralSeries₂, IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat, toEnd_eq_iff, isNilpotent_toEnd_of_mem_rootSpace, toEnd_lie, LieAlgebra.toEnd_pow_apply_mem, isRegular_iff_natTrailingDegree_charpoly_eq_rank, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, toEnd_pow_lie, LieSubmodule.coe_toEnd, toEnd_apply_apply, commute_toEnd_of_mem_center_right, toEnd_baseChange, isNilpotent_iff_forall, isNilpotent_toEnd_sub_algebraMap, IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, toEnd_eq_zero_iff, traceForm_apply_apply, trace_toEnd_genWeightSpaceChain_eq_zero, maxGenEigenSpace_toEnd_eq_top, isNilpotent_iff_forall', LieSubmodule.coe_toEnd_pow, mem_genWeightSpaceOf, coe_lcs_range_toEnd_eq, toEnd_module_end, LieAlgebra.mem_zeroRootSubalgebra, iterate_toEnd_mem_lowerCentralSeries, commute_toEnd_of_mem_center_left, Weight.hasEigenvalueAt, rank_le_natTrailingDegree_charpoly_ad, toEnd_matrix, toEnd_pow_comp_lieHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_of_isFaithful 📖	—	Bracket.bracket LieRingModule.toBracket	—	—	smulCommClass_self IsScalarTower.left toEnd_eq_iff LinearMap.ext
instIsFaithfulEnd 📖	mathematical	—	IsFaithful Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.End.instLieRingModule Module.End.instLieModule	—	smulCommClass_self IsScalarTower.left Module.End.instLieModule toEnd_module_end
instIsFaithfulSubtypeMemLieSubalgebra 📖	mathematical	—	IsFaithful LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieRing LieSubalgebra.lieAlgebra LieSubalgebra.lieRingModule LieSubalgebra.lieModule	—	LieSubalgebra.lieModule smulCommClass_self IsScalarTower.left IsFaithful.injective_toEnd Subtype.val_injective
isFaithful_iff 📖	mathematical	—	IsFaithful Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd	—	smulCommClass_self IsScalarTower.left
isFaithful_iff' 📖	mathematical	—	IsFaithful NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	smulCommClass_self IsScalarTower.left LinearMap.ext sub_eq_zero sub_lie toEnd_apply_apply
ofAssociativeModule 📖	mathematical	—	LieModule LieRing.ofAssociativeRing LieAlgebra.ofAssociativeAlgebra LieRingModule.ofAssociativeModule	—	smul_assoc smul_algebra_smul_comm
toEnd_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LieHom Module.End LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd Bracket.bracket LieRingModule.toBracket	—	smulCommClass_self IsScalarTower.left
toEnd_eq_iff 📖	mathematical	—	DFunLike.coe LieHom Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd	—	smulCommClass_self IsScalarTower.left IsFaithful.injective_toEnd
toEnd_eq_zero_iff 📖	mathematical	—	DFunLike.coe LieHom Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	smulCommClass_self IsScalarTower.left LinearMap.map_zero toEnd_eq_iff
toEnd_lie 📖	mathematical	—	DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd Bracket.bracket LieRingModule.toBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LieRing.toAddCommGroup LieAlgebra.toModule LieAlgebra.ad	—	smulCommClass_self IsScalarTower.left lie_lie sub_add_cancel
toEnd_module_end 📖	mathematical	—	toEnd Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.End.instLieRingModule Module.End.instLieModule LieHom.id	—	LieHom.ext smulCommClass_self IsScalarTower.left Module.End.instLieModule LinearMap.ext
toEnd_pow_apply_map 📖	mathematical	—	DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd LieModuleHom LieModuleHom.instFunLike	—	LinearMap.congr_fun RingHomCompTriple.ids smulCommClass_self IsScalarTower.left toEnd_pow_comp_lieHom
toEnd_pow_comp_lieHom 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Module.End Monoid.toNatPow Module.End.instMonoid DFunLike.coe LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd LieModuleHom.toLinearMap	—	Module.End.commute_pow_left_of_commute smulCommClass_self IsScalarTower.left LinearMap.ext RingHomCompTriple.right_ids RingHomCompTriple.ids LieModuleHom.map_lie
toEnd_pow_lie 📖	mathematical	—	DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd Bracket.bracket LieRingModule.toBracket Finset.sum Finset.HasAntidiagonal.antidiagonal Nat.instAddMonoid Finset.Nat.instHasAntidiagonal AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Nat.choose LieRing.toAddCommGroup LieAlgebra.toModule LieAlgebra.ad	—	smulCommClass_self IsScalarTower.left pow_zero Finset.sum_congr Finset.antidiagonal_zero Nat.instCanonicallyOrderedAdd Finset.sum_singleton Nat.choose_self one_smul Finset.sum_antidiagonal_choose_succ_nsmul pow_succ' map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_nsmul toEnd_lie nsmul_add Finset.sum_add_distrib add_comm add_left_cancel_iff AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.choose_symm_of_eq_add Finset.HasAntidiagonal.mem_antidiagonal

LieModule.IsFaithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_toEnd 📖	mathematical	—	Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd	—	—

LieRing

Definitions

Name	Category	Theorems
ofAssociativeRing 📖	CompOp	279 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, LieRinehartRing.lie_smul_eq_mul, RootPairing.GeckConstruction.isSl2Triple, LieAlgebra.IsKilling.restrict_killingForm_eq_sum, LieSubmodule.lowerCentralSeries_tensor_eq_baseChange, LieModule.toEnd_pow_apply_map, skewAdjointMatricesLieSubalgebraEquivTranspose_apply, RootPairing.GeckConstruction.instHasTrivialRadical, LieAlgebra.Orthogonal.mem_so, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, LieModule.trace_toEnd_eq_zero_of_mem_lcs, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, Matrix.lieConj_apply, LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, Matrix.isSkewAdjoint_bracket, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LieAlgebra.finrank_engel, skewAdjointLieSubalgebraEquiv_apply, LieModule.traceForm_eq_sum_finrank_nsmul', LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.IsKilling.rootSystem_coroot_apply, LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, LeftInvariantDerivation.left_invariant, LieModule.instIsFaithfulMatrixForall, LieSubalgebra.toEnd_eq, LieAlgebra.lieCharacterEquivLinearDual_apply, LieModule.isNilpotent_toEnd_genWeightSpace_zero, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, LieModule.ofAssociativeModule, skewAdjointLieSubalgebraEquiv_symm_apply, LieModule.trace_toEnd_genWeightSpace, AlgHom.toLieHom_id, UniversalEnvelopingAlgebra.lift_unique, LieModule.shiftedGenWeightSpace.toEnd_eq, LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, Module.End.instLieModule, LieRinehartAlgebra.Hom.anchor_derivation, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieSubmodule.Quotient.toEnd_comp_mk', LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieModule.mem_posFittingCompOf, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, LieModule.isNilpotent_range_toEnd_iff, LieAlgebra.rank_le_natTrailingDegree_charpoly_ad, LieSubmodule.lie_top_eq_of_span_sup_eq_top, Derivation.bracket_eq_fun, LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, LieAlgebra.ad_eq_lmul_left_sub_lmul_right, two_nsmul_lie_lmul_lmul_add_add_eq_zero, LieModule.isNilpotent_toEnd_of_isNilpotent, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, commutative_ring_iff_abelian_lie_ring, LieModule.genWeightSpaceChain_neg, LieSubmodule.coe_map_toEnd_le, LieModule.mem_genWeightSpace, LieAlgebra.LoopAlgebra.toFinsupp_symm_single, LieRinehartRing.leibniz_mul_right, UniversalEnvelopingAlgebra.ι_comp_lift, LieModule.Weight.coe_coe, lie_apply, LieSubalgebra.toEnd_mk, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton', LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, LeftInvariantDerivation.evalAt_coe, LieModule.coe_genWeightSpaceOf_zero, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, LieSubmodule.traceForm_eq_zero_of_isTrivial, lieEquivMatrix'_apply, LieModule.weight_vector_multiplication, LieSubalgebra.coe_ad_pow, Derivation.instLieModule, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.lieCharacterEquivLinearDual_symm_apply, LieAlgebra.instIsSolvableTensorProduct, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LinearMap.BilinForm.lieInvariant_iff, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, Matrix.instLieModuleForall, LieModule.isFaithful_iff, LieSubmodule.toEnd_comp_subtype_mem, LieAlgebra.ad_nilpotent_of_nilpotent, LieModule.rank_eq_natTrailingDegree, LieSubmodule.mem_baseChange_iff, LieAlgebra.ad_pow_lie, LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup, LieModule.isNilpotent_toEnd_of_isNilpotent₂, RootPairing.GeckConstruction.span_range_h'_eq_top, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, LieModule.Weight.coe_toLinear_eq_zero_iff, LieAlgebra.IsKilling.coroot_mem_corootSpace, Derivation.commutator_coe_linear_map, LieAlgebra.IsKilling.apply_coroot_eq_cast, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieModule.exists_forall_pow_toEnd_eq_zero, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, JacobsonNoether.exist_pow_eq_zero_of_le, Matrix.reindexLieEquiv_apply, LieAlgebra.SpecialLinear.sl_bracket, LieSubmodule.toEnd_restrict_eq_toEnd, Matrix.reindexLieEquiv_symm, UniversalEnvelopingAlgebra.lift_ι_apply, LieModule.IsFaithful.injective_toEnd, RootPairing.GeckConstruction.span_range_h_le_range_diagonal, LieModule.instIsNilpotentTensor, AlgEquiv.toLieEquiv_symm_apply, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply, LieModule.lie_traceForm_eq_zero, mem_skewAdjointMatricesLieSubalgebra, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, Matrix.lieConj_symm_apply, of_associative_ring_bracket, LieModule.trace_comp_toEnd_genWeightSpace_eq, RootPairing.GeckConstruction.ω_mul_h, Module.End.lie_apply, RootPairing.GeckConstruction.instIsIrreducible, killingForm_apply_apply, LieSubalgebra.mem_engel_iff, two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add, LieModule.iterate_toEnd_mem_lowerCentralSeries₂, LieSubmodule.lie_baseChange, LieAlgebra.Orthogonal.s_as_blocks, IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat, LieModule.toEnd_eq_iff, LinearEquiv.lieConj_apply, LieModule.isNilpotent_toEnd_of_mem_rootSpace, UniversalEnvelopingAlgebra.lift_symm_apply, LieAlgebra.derivedSeries_baseChange, LieDerivation.toLinearMapLieHom_injective, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, Matrix.lie_apply, LieModule.toEnd_lie, LieAlgebra.ExtendScalars.bracket_tmul, LieRinehartRing.leibniz_smul_right, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieAlgebra.LoopAlgebra.toFinsupp_single_tmul, LieAlgebra.ad_apply, LieAlgebra.toEnd_pow_apply_mem, LieAlgebra.lieCharacter_apply_of_mem_derived, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, LieModule.traceForm_eq_sum_finrank_nsmul, LieAlgebra.conj_ad_apply, LieSubmodule.tmul_mem_baseChange_of_mem, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, LieAlgebra.IsKilling.span_weight_isNonZero_eq_top, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, RootPairing.GeckConstruction.ωConj_invFun, LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, LieDerivation.commutator_coe_linear_map, UniversalEnvelopingAlgebra.ι_apply, LieModule.toEnd_pow_lie, LieSubmodule.coe_toEnd, LieModule.toEnd_apply_apply, mem_skewAdjointMatricesLieSubalgebra_unit_smul, LieModule.commute_toEnd_of_mem_center_right, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff, LieModule.toEnd_baseChange, RootPairing.GeckConstruction.f_lie_v_ne, LieAlgebra.matrix_trace_commutator_zero, RootPairing.GeckConstruction.ωConj_toFun, RootPairing.GeckConstruction.e_lie_v_ne, LieAlgebra.IsKilling.eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul, LieAlgebra.SpecialLinear.val_single, LieModule.isNilpotent_iff_forall, LieModule.isNilpotent_toEnd_sub_algebraMap, LieAlgebra.LoopAlgebra.residuePairing_apply_apply, lieEquivMatrix'_symm_apply, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, RootPairing.GeckConstruction.h_mem_lieAlgebra, AlgHom.coe_toLieHom, LieModule.chainTop_neg, LieModule.chainBot_neg, IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieAlgebra.IsKilling.rootSystem_pairing_apply, LieAlgebra.IsKilling.chainTopCoeff_zero_right, Matrix.lie_transpose, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieModule.toEnd_eq_zero_iff, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, LieAlgebra.isNilpotent_ad_of_mem_rootSpace, AlgHom.toLieHom_comp, LieModule.traceForm_apply_apply, LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, lie_eq_smul, LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add, RootPairing.GeckConstruction.lie_e_lie_f_apply, LieModule.maxGenEigenSpace_toEnd_eq_top, LinearEquiv.lieConj_symm, LieAlgebra.rank_eq_natTrailingDegree, LieAlgebra.IsKilling.chainBotCoeff_le_chainLength, LieAlgebra.mem_corootSpace', LieAlgebra.ad_lie, RootPairing.GeckConstruction.f_lie_v_same, LieModule.isNilpotent_iff_forall', LeftInvariantDerivation.evalAt_mul, LieSubmodule.coe_toEnd_pow, LieAlgebra.isNilpotent_range_ad_iff, LieModule.mem_genWeightSpaceOf, LieAlgebra.IsKilling.traceForm_coroot, LieModule.chainBotCoeff_neg, LieModule.traceForm_eq_sum_finrank_nsmul_mul, UniversalEnvelopingAlgebra.hom_ext_iff, LieAlgebra.nilpotent_ad_of_nilpotent_algebra, Derivation.commutator_apply, LieModule.instIsFaithfulEnd, LieAlgebra.IsKilling.chainBotCoeff_zero_right, LieAlgebra.derivedSeriesOfIdeal_baseChange, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieModule.coe_lcs_range_toEnd_eq, LieModule.toEnd_module_end, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.ExtendScalars.instLieModule, LieRinehartAlgebra.Hom.apply_lie', LieAlgebra.mem_corootSpace, LieModule.iterate_toEnd_mem_lowerCentralSeries, LieAlgebra.isSolvable_tensorProduct_iff, RootPairing.GeckConstruction.f_mem_lieAlgebra, LieAlgebra.lieCharacter_apply_lie, LieRinehartAlgebra.instDerivation, LieAlgebra.IsKilling.chainTopCoeff_le_chainLength, LieDerivation.coe_ad_apply_eq_ad_apply, LieAlgebra.lieCharacter_apply_lie', RootPairing.GeckConstruction.e_mem_lieAlgebra, LieAlgebra.SpecialLinear.val_singleSubSingle, LieAlgebra.isNilpotent_iff_forall, LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical, LieAlgebra.IsKilling.span_weight_eq_top, skewAdjointMatricesLieSubalgebraEquiv_apply, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, LieModule.traceForm_apply_lie_apply', LieModule.Weight.toLinear_neg, LieSubmodule.coe_baseChange, LieAlgebra.Extension.twoCocycleOf_coe_coe, LieModule.chainTopCoeff_neg, AlgEquiv.toLieEquiv_apply, LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero, AlgHom.toLieHom_apply, LieSubmodule.baseChange_top, LieModule.commute_toEnd_of_mem_center_left, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LieAlgebra.ad_ker_eq_self_module_ker, LieModule.range_traceForm_le_span_weight, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieModule.genWeightSpace_neg_add_chainBot, RootPairing.GeckConstruction.lie_e_f_mul_ω, LieAlgebra.ExtendScalars.map_apply_tmul, LieRinehartAlgebra.toLieModule, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.IsKilling.rootSystem_root_apply, LieModule.Weight.coe_neg, UniversalEnvelopingAlgebra.lift_ι_apply', RootPairing.GeckConstruction.e_lie_u, LieRinehartAlgebra.Hom.apply_lie, LieModule.Weight.instLinearMapClass, LieModule.Weight.hasEigenvalueAt, LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton, LieRinehartAlgebra.instLieRinehartRingDerivation, LieModule.rank_le_natTrailingDegree_charpoly_ad, LieSubalgebra.coe_ad, LieModule.toEnd_matrix, LieModule.Weight.toLinear_apply, LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, LieModule.toEnd_pow_comp_lieHom, LieAlgebra.SpecialLinear.sl_non_abelian, LieSubmodule.baseChange_bot, LeftInvariantDerivation.evalAt_apply, LieSubalgebra.ad_comp_incl_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lie_apply 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket ofAssociativeRing Pi.ring toAddCommGroup lieRingSelfModule	—	—
of_associative_ring_bracket 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket ofAssociativeRing toAddCommGroup lieRingSelfModule SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—

LieRingModule

Definitions

Name	Category	Theorems
ofAssociativeModule 📖	CompOp	2 math math: LieModule.ofAssociativeModule, lie_eq_smul

LieSubalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ad_comp_incl_eq 📖	mathematical	—	LinearMap.comp LieSubalgebra SetLike.instMembership instSetLike CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup lieRing LieAlgebra.toModule lieAlgebra RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe LieHom Module.End LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieAlgebra.ad LieHom.toLinearMap incl	—	LinearMap.ext RingHomCompTriple.ids smulCommClass_self IsScalarTower.left
coe_ad 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup lieRing LieAlgebra.toModule lieAlgebra LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieAlgebra.ad	—	smulCommClass_self IsScalarTower.left
coe_ad_pow 📖	mathematical	—	LieSubalgebra SetLike.instMembership instSetLike DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup lieRing LieAlgebra.toModule lieAlgebra LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieAlgebra.ad	—	LieSubmodule.coe_toEnd_pow lieModule lieAlgebraSelfModule
toEnd_eq 📖	mathematical	—	DFunLike.coe LieHom LieSubalgebra SetLike.instMembership instSetLike Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid lieRing lieAlgebra LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd lieRingModule lieModule	—	smulCommClass_self IsScalarTower.left lieModule
toEnd_mk 📖	mathematical	LieSubalgebra SetLike.instMembership instSetLike	DFunLike.coe LieHom Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid lieRing lieAlgebra LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd lieRingModule lieModule	—	smulCommClass_self IsScalarTower.left lieModule

LieSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_map_toEnd_le 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LieHom Module.End LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd toSubmodule	—	RingHomSurjective.ids smulCommClass_self IsScalarTower.left lie_mem
coe_toEnd 📖	mathematical	—	LieSubmodule SetLike.instMembership instSetLike DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup instSMulMemClass LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd instLieRingModuleSubtypeMem instLieModule	—	instAddSubgroupClass instSMulMemClass smulCommClass_self IsScalarTower.left instLieModule
coe_toEnd_pow 📖	mathematical	—	LieSubmodule SetLike.instMembership instSetLike DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddSubgroupClass.toAddCommGroup instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup instSMulMemClass LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd instLieRingModuleSubtypeMem instLieModule	—	instAddSubgroupClass instSMulMemClass smulCommClass_self IsScalarTower.left instLieModule pow_succ'
mapsTo_pow_toEnd_sub_algebraMap 📖	mathematical	—	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid LinearMap.instSub LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd RingHom Module.End.instSemiring RingHom.instFunLike algebraMap SetLike.coe LieSubmodule instSetLike	—	smulCommClass_self IsScalarTower.left Module.End.coe_pow Set.MapsTo.iterate Submodule.sub_mem lie_mem Submodule.smul_mem
toEnd_comp_subtype_mem 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike toSubmodule	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike LinearMap.comp RingHomCompTriple.ids LieHom Module.End LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd Submodule.subtype	—	RingHomCompTriple.ids smulCommClass_self IsScalarTower.left lie_mem
toEnd_restrict_eq_toEnd 📖	mathematical	toEnd_comp_subtype_mem	LinearMap.restrict CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LieHom Module.End LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd toSubmodule LieSubmodule SetLike.instMembership instSetLike AddSubgroupClass.toAddCommGroup instAddSubgroupClass SubmoduleClass.module AddCommGroup.toAddGroup instSMulMemClass instLieRingModuleSubtypeMem instLieModule	—	RingHomCompTriple.ids smulCommClass_self IsScalarTower.left

LinearEquiv

Definitions

Name	Category	Theorems
lieConj 📖	CompOp	4 math math: skewAdjointLieSubalgebraEquiv_apply, skewAdjointLieSubalgebraEquiv_symm_apply, lieConj_apply, lieConj_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieConj_apply 📖	mathematical	—	DFunLike.coe LieEquiv Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike LieEquiv.instEquivLike lieConj LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module CommSemiring.toCommMonoid DFinsupp.instEquivLikeLinearEquiv conj	—	RingHomInvPair.ids smulCommClass_self IsScalarTower.left
lieConj_symm 📖	mathematical	—	LieEquiv.symm Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero lieConj symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids	—	RingHomInvPair.ids smulCommClass_self IsScalarTower.left

Module.End

Definitions

Name	Category	Theorems
instLieRingModule 📖	CompOp	10 math math: LinearMap.BilinForm.isSkewAdjoint_bracket, instLieModule, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieModule.isNilpotent_range_toEnd_iff, Derivation.commutator_coe_linear_map, lie_apply, LieDerivation.commutator_coe_linear_map, LieModule.instIsFaithfulEnd, LieModule.coe_lcs_range_toEnd_eq, LieModule.toEnd_module_end

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLieModule 📖	mathematical	—	LieModule Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.ofAssociativeRing instRing LieAlgebra.ofAssociativeAlgebra instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero instLieRingModule	—	LieModule.ofAssociativeModule smulCommClass_self IsScalarTower.left apply_isScalarTower
lie_apply 📖	mathematical	—	Bracket.bracket Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRingModule.toBracket LieRing.ofAssociativeRing instRing instLieRingModule DFunLike.coe LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring	—	—

(root)

Definitions

Name	Category	Theorems
lieSubalgebraOfSubalgebra 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lie_eq_smul 📖	mathematical	—	Bracket.bracket LieRingModule.toBracket LieRing.ofAssociativeRing LieRingModule.ofAssociativeModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	—

---

← Back to Index