Lemmas

📁 Source: Mathlib/Algebra/Lie/Semisimple/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems hasCentralRadical_and_of_isIrreducible_of_isFaithful, hasTrivialRadical_of_isIrreducible_of_isFaithful, trace_toEnd_eq_zero	3
Total	3

LieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCentralRadical_and_of_isIrreducible_of_isFaithful 📖	mathematical	—	HasCentralRadical EuclideanDomain.toCommRing Field.toEuclideanDomain LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup toModule lieRingSelfModule center Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule LinearMap RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Submodule.setLike Submodule.span Set Set.instSingletonSet LinearMap.id DFunLike.coe LieHom LieRing.ofAssociativeRing Module.End.instRing ofAssociativeAlgebra Module.End.instAlgebra Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike LieModule.toEnd	—	LieModule.nontrivial_of_isIrreducible LieIdeal.lieModule smulCommClass_self IsScalarTower.left LieModule.exists_nontrivial_weightSpace_of_isSolvable radicalIsSolvable isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule LieModule.instIsTriangularizableSubtypeMemLieSubmodule instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsDomain LieSubmodule.instAddSubgroupClass Module.free_of_finite_type_torsion_free' instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors instIsLieTowerSubtypeMemLieSubmodule_1 instIsLieTowerSubtypeMemLieSubmodule LieSubmodule.eq_top_of_isIrreducible LinearMap.ext LieIdeal.coe_bracket_of_module LieSubmodule.mem_top le_antisymm lieAlgebraSelfModule LieModule.mem_maxTrivSubmodule LieModule.toEnd_eq_zero_iff LieHom.map_lie Module.End.instLieModule lie_smul LinearMap.instLieModule Commute.lie_eq Module.End.commute_id_right smul_zero center_le_radical Submodule.mem_span_singleton
hasTrivialRadical_of_isIrreducible_of_isFaithful 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule LinearMap.instFunLike LinearMap.trace LieHom Module.End CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain 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 LieModule.toEnd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	HasTrivialRadical	—	smulCommClass_self IsScalarTower.left LT.lt.ne' Module.finrank_pos_iff commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors LieModule.nontrivial_of_isIrreducible hasCentralRadical_and_of_isIrreducible_of_isFaithful hasTrivialRadical_iff hasCentralRadical_iff LieSubmodule.eq_bot_iff Submodule.mem_span_singleton map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.trace_id Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule IsDomain.to_noZeroDivisors LieModule.toEnd_eq_zero_iff zero_smul
trace_toEnd_eq_zero 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule LinearMap.instFunLike LinearMap.trace LieHom Module.End 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 LieModule.toEnd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LieSubalgebra SetLike.instMembership LieSubalgebra.instSetLike LieSubalgebra.lieSpan	—	—	smulCommClass_self IsScalarTower.left LieSubalgebra.lieSpan_induction map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass add_zero map_smul SemilinearMapClass.toMulActionSemiHomClass MulZeroClass.mul_zero LieHom.map_lie LinearMap.trace_lie

---

← Back to Index