LieTheorem

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

Statistics

Metric	Count
Definitions weightSpaceOfIsLieTower	1
Theorems exists_nontrivial_weightSpace_of_isSolvable, exists_nontrivial_weightSpace_of_lieIdeal	2
Total	3

LieModule

Definitions

Name	Category	Theorems
weightSpaceOfIsLieTower 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nontrivial_weightSpace_of_isSolvable 📖	mathematical	—	Nontrivial LieSubmodule EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership LieSubmodule.instSetLike weightSpace DFunLike.coe Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id	—	smulCommClass_self IsScalarTower.left LinearMap.instIsScalarTower RingHomSurjective.ids LinearMap.mem_range LieSubalgebra.lieModule Module.End.instLieModule LieHom.isSolvable_range instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite LieSubalgebra.instIsNoetherianSubtypeMem isNoetherian_linearMap isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule Module.Projective.of_free Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors RingHomCompTriple.ids AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass exists_ne nontrivial_of_ne mem_weightSpace
exists_nontrivial_weightSpace_of_lieIdeal 📖	mathematical	IsCoatom Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instOrderTop LieSubmodule.toSubmodule lieRingSelfModule	Nontrivial LieSubmodule SetLike.instMembership LieSubmodule.instSetLike weightSpace DFunLike.coe Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id	—	LieIdeal.lieModule SetLike.exists_of_lt instIsConcreteLE IsCoatom.lt_top RingHomInvPair.ids instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass LinearEquiv.toSpanNonzeroSingleton_symm_apply_smul Submodule.isCompl_span_singleton_of_isCoatom_of_notMem IsCompl.symm instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.free_of_finite_type_torsion_free' instIsLieTowerSubtypeMemLieSubmodule_1 instIsLieTowerSubtypeMemLieSubmodule LieSubmodule.instSMulMemClass smulCommClass_self IsScalarTower.left LieSubmodule.instLieModule Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top IsTriangularizable.maxGenEigenspace_eq_top instIsTriangularizableSubtypeMemLieSubmodule_1 Module.End.HasEigenvalue.exists_hasEigenvector LieIdeal.coe_bracket_of_module RingHomCompTriple.ids Algebra.to_smulCommClass nontrivial_of_ne mem_weightSpace Submodule.IsCompl.projection_add_projection_eq_self Submodule.IsCompl.projection_apply smul_lie Module.End.HasEigenvector.apply_eq_smul smul_assoc SMulCommClass.smul_comm add_lie add_smul

---

← Back to Index