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	30 math math: finrank_engel, isRegular_iff_natTrailingDegree_charpoly_eq_rank, ad_isSemisimple_of_isSemisimple, 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, LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad, 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, commute_ad_of_commute, 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	260 math math: IsKilling.rootSystem_toLinearMap_apply, RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', 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, LieIdeal.reflectionPerm_mem_rootSet_iff, LieModule.instIsFaithfulMatrixForall, LieSubalgebra.toEnd_eq, Lie.Derivation.ofLieDerivation_apply, 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, ad_isSemisimple_of_isSemisimple, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, Module.End.instLieModule, LieSubmodule.Quotient.toEnd_comp_mk', LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieIdeal.toInvtRootSubmodule_mono, LieModule.mem_posFittingCompOf, SpecialLinear.singleSubSingle_add_singleSubSingle, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, LieModule.isNilpotent_range_toEnd_iff, rank_le_natTrailingDegree_charpoly_ad, AdicCompletion.ofPowSMul_ofValEqZero, 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, Basis.linearIndepOn_root_baseSupp, LieSubmodule.coe_map_toEnd_le, LieModule.mem_genWeightSpace, LoopAlgebra.toFinsupp_symm_single, LieIdeal.rootSpan_mem_invtRootSubmodule, Basis.coroot_eq_h', UniversalEnvelopingAlgebra.ι_comp_lift, LieModule.Weight.coe_coe, LieSubalgebra.toEnd_mk, 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, LieModule.lie_mem_maxGenEigenspace_toEnd, LinearMap.BilinForm.lieInvariant_iff, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, Matrix.instLieModuleForall, LieSubmodule.trace_eq_trace_restrict_of_le_idealizer, LieModule.isFaithful_iff, LieRinehartAlgebra.anchor_apply, Derivation.Compatible.mem, LieSubmodule.toEnd_comp_subtype_mem, ad_nilpotent_of_nilpotent, LieModule.rank_eq_natTrailingDegree, LieSubmodule.mem_baseChange_iff, trace_toEnd_eq_zero, 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', RootPairing.GeckConstruction.basis_A_eq, LieModule.exists_forall_pow_toEnd_eq_zero, IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, JacobsonNoether.exist_pow_eq_zero_of_le, Matrix.reindexLieEquiv_apply, IsKilling.isSimple_iff_isIrreducible, SpecialLinear.sl_bracket, LieSubmodule.toEnd_restrict_eq_toEnd, Matrix.reindexLieEquiv_symm, UniversalEnvelopingAlgebra.lift_ι_apply, AdicCompletion.ofPowSMul_injective, 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₂, Derivation.Compatible.apply, 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, AdicCompletion.ofPowSMul_val_apply_eq_zero, IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad, 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, LieRinehartAlgebra.anchor_derivation, LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank, RootPairing.GeckConstruction.h_mem_cartanSubalgebra', 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, Basis.cartanMatrix_base_eq, 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, AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval, 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, Lie.Derivation.ofDerivation_apply, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, RootPairing.GeckConstruction.ωConj_mem_of_mem, LieModule.maxGenEigenSpace_toEnd_eq_top, LinearEquiv.lieConj_symm, rank_eq_natTrailingDegree, IsKilling.lieIdealOrderIso_right_inv, ad_lie, LieModule.isNilpotent_iff_forall', LeftInvariantDerivation.evalAt_mul, LieSubmodule.coe_toEnd_pow, isNilpotent_range_ad_iff, LieModule.mem_genWeightSpaceOf, IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, IsKilling.traceForm_coroot, UniversalEnvelopingAlgebra.hom_ext_iff, nilpotent_ad_of_nilpotent_algebra, Derivation.commutator_apply, LieModule.instIsFaithfulEnd, IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, derivedSeriesOfIdeal_baseChange, Basis.root_mem_or_mem_neg, LieModule.coe_lcs_range_toEnd_eq, LieModule.toEnd_module_end, mem_zeroRootSubalgebra, IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, ExtendScalars.instLieModule, commute_ad_of_commute, 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, RootPairing.GeckConstruction.linearIndependent_h, skewAdjointMatricesLieSubalgebraEquiv_apply, LoopAlgebra.twoCocycleOfBilinear_coe, isNilpotent_ad_of_isNilpotent, LieModule.Weight.toLinear_neg, LieSubmodule.coe_baseChange, Extension.twoCocycleOf_coe_coe, Derivation.Compatible.mk_left, AdicCompletion.ofPowSMul_val_apply, 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, Basis.coe_baseSupportEquiv_apply, Basis.linearIndependent_baseSupp, 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, Derivation.Compatible.mk_right, 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.toPow 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.toNSMul 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	71 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, lie_mem_maxGenEigenspace_toEnd, IsTriangularizable.maxGenEigenspace_eq_top, LieSubmodule.trace_eq_trace_restrict_of_le_idealizer, isFaithful_iff, LieSubmodule.toEnd_comp_subtype_mem, rank_eq_natTrailingDegree, LieAlgebra.trace_toEnd_eq_zero, 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.toPow 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.toPow 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.toPow 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.toNSMul 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	331 math math: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', RootPairing.GeckConstruction.isSl2Triple, LinearMap.BilinForm.isSkewAdjoint_bracket, 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, LieAlgebra.Orthogonal.soIndefiniteEquiv_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, LieIdeal.reflectionPerm_mem_rootSet_iff, LieAlgebra.Basis.borelLower_le_biSup, LieModule.instIsFaithfulMatrixForall, LieSubalgebra.toEnd_eq, Lie.Derivation.ofLieDerivation_apply, LieAlgebra.lieCharacterEquivLinearDual_apply, LieModule.isNilpotent_toEnd_genWeightSpace_zero, Representation.char_dual, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, LieRinehartAlgebra.LieRinehartRing.leibniz_smul_right, LieModule.ofAssociativeModule, skewAdjointLieSubalgebraEquiv_symm_apply, LieModule.trace_toEnd_genWeightSpace, AlgHom.toLieHom_id, UniversalEnvelopingAlgebra.lift_unique, LieModule.shiftedGenWeightSpace.toEnd_eq, LieAlgebra.ad_isSemisimple_of_isSemisimple, LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, Module.End.instLieModule, LieAlgebra.IsKilling.apply_coroot_eq_cast', LieSubmodule.Quotient.toEnd_comp_mk', LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieIdeal.toInvtRootSubmodule_mono, LieModule.mem_posFittingCompOf, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, LieModule.isNilpotent_range_toEnd_iff, LieAlgebra.rank_le_natTrailingDegree_charpoly_ad, AdicCompletion.ofPowSMul_ofValEqZero, 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, LieAlgebra.Basis.linearIndepOn_root_baseSupp, LieModule.genWeightSpaceChain_neg, LieSubmodule.coe_map_toEnd_le, LieModule.mem_genWeightSpace, LieAlgebra.LoopAlgebra.toFinsupp_symm_single, LieIdeal.rootSpan_mem_invtRootSubmodule, LieAlgebra.Basis.coroot_eq_h', UniversalEnvelopingAlgebra.ι_comp_lift, LieModule.Weight.coe_coe, lie_apply, LieSubalgebra.toEnd_mk, LieAlgebra.Basis.symm_baseSupp, 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, LieRinehartRing.lie_smul_eq_mul', Derivation.instLieModule, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, LieAlgebra.lieCharacterEquivLinearDual_symm_apply, LieAlgebra.instIsSolvableTensorProduct, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieModule.lie_mem_maxGenEigenspace_toEnd, LinearMap.BilinForm.lieInvariant_iff, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, Matrix.instLieModuleForall, LieSubmodule.trace_eq_trace_restrict_of_le_idealizer, LieModule.isFaithful_iff, LieRinehartAlgebra.anchor_apply, Derivation.Compatible.mem, LieSubmodule.toEnd_comp_subtype_mem, LieAlgebra.ad_nilpotent_of_nilpotent, LieModule.rank_eq_natTrailingDegree, LieSubmodule.mem_baseChange_iff, LieAlgebra.trace_toEnd_eq_zero, 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.Basis.iSupIndep_rootSpace, LieRinehartRing.leibniz_smul_right', LieAlgebra.IsKilling.apply_coroot_eq_cast, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', RootPairing.GeckConstruction.basis_A_eq, LieModule.exists_forall_pow_toEnd_eq_zero, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, JacobsonNoether.exist_pow_eq_zero_of_le, Matrix.reindexLieEquiv_apply, LieAlgebra.IsKilling.isSimple_iff_isIrreducible, LieAlgebra.SpecialLinear.sl_bracket, LieSubmodule.toEnd_restrict_eq_toEnd, Matrix.reindexLieEquiv_symm, UniversalEnvelopingAlgebra.lift_ι_apply, AdicCompletion.ofPowSMul_injective, 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₂, Derivation.Compatible.apply, 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, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg, LieModule.toEnd_lie, LieAlgebra.ExtendScalars.bracket_tmul, AdicCompletion.ofPowSMul_val_apply_eq_zero, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux, LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad, 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, LieRinehartAlgebra.anchor_derivation, LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank, RootPairing.GeckConstruction.h_mem_cartanSubalgebra', 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, LieRinehartAlgebra.LieRinehartRing.leibniz_mul_right, 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, LieAlgebra.Basis.cartanMatrix_base_eq, 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, AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval, 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, Lie.Derivation.ofDerivation_apply, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, lie_eq_smul, RootPairing.GeckConstruction.ωConj_mem_of_mem, 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.IsKilling.lieIdealOrderIso_right_inv, 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.coe_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.IsKilling.traceForm_coroot, LieAlgebra.Basis.borelLower_eq, FDRep.char_dual, 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.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, LieAlgebra.derivedSeriesOfIdeal_baseChange, LieAlgebra.Basis.root_mem_or_mem_neg, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff, LieAlgebra.Orthogonal.pso_inv, LieModule.coe_lcs_range_toEnd_eq, LieModule.toEnd_module_end, LieAlgebra.mem_zeroRootSubalgebra, LieAlgebra.IsKilling.restr_invtSubmoduleToLieIdeal_eq_iSup, LieAlgebra.ExtendScalars.instLieModule, LieAlgebra.commute_ad_of_commute, 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, LieRinehartRing.leibniz_mul_right', 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, RootPairing.GeckConstruction.linearIndependent_h, skewAdjointMatricesLieSubalgebraEquiv_apply, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, LieModule.traceForm_apply_lie_apply', LieAlgebra.Basis.coe_linearMap_baseSupp', LieAlgebra.isNilpotent_ad_of_isNilpotent, LieModule.Weight.toLinear_neg, LieSubmodule.coe_baseChange, LieAlgebra.Extension.twoCocycleOf_coe_coe, LieModule.chainTopCoeff_neg, Derivation.Compatible.mk_left, AdicCompletion.ofPowSMul_val_apply, 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.Basis.coe_baseSupportEquiv_apply, LieAlgebra.Basis.linearIndependent_baseSupp, LieAlgebra.ad_ker_eq_self_module_ker, LieRinehartAlgebra.LieRinehartRing.lie_smul_eq_mul, 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, Derivation.Compatible.mk_right, 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.toPow 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 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

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.toPow 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.toPow 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	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