Semisimple

📁 Source: Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean

Statistics

Metric	Count
Definitions	0
Theorems genEigenspace_eq_eigenspace, maxGenEigenspace_eq_eigenspace, eq_zero_iff_forall_eigenvalue, iSup_eigenspace_eq_top, apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil	5
Total	5

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike DFunLike.coe OrderHom ENat instPreorderENat PartialOrder.toPreorder Submodule.instPartialOrder OrderHom.instFunLike genEigenspace Commute Module.End instMul IsFinitelySemisimple IsNilpotent LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toPow instMonoid LinearMap.instSub	DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smulCommClass_self mem_genEigenspace mapsTo_genEigenspace_of_comm IsScalarTower.left Commute.sub_right Algebra.commute_algebraMap_right Algebra.mul_sub_algebraMap_commutes Commute.sub_left Algebra.commute_algebraMap_left Submodule.sub_mem sub_sub_sub_cancel_left LinearMap.restrict_sub LinearMap.restrict.congr_simp Commute.isNilpotent_sub LinearMap.restrict_commute isNilpotent_restrict_sub_algebraMap isNilpotent.restrict Submodule.isScalarTower' eq_zero_of_isNilpotent_of_isFinitelySemisimple IsFinitelySemisimple.restrict mem_genEigenspace_nat SMulMemClass.smul_mem Submodule.smulMemClass LinearMap.congr_fun

Module.End.IsFinitelySemisimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
genEigenspace_eq_eigenspace 📖	mathematical	Module.End.IsFinitelySemisimple ENat instLTENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instPreorderENat PartialOrder.toPreorder Submodule.instPartialOrder OrderHom.instFunLike Module.End.genEigenspace Module.End.eigenspace	—	le_antisymm Module.End.mem_eigenspace_iff Module.End.apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil sub_self OrderHom.mono Order.one_le_iff_pos NeZero.charZero_one
maxGenEigenspace_eq_eigenspace 📖	mathematical	Module.End.IsFinitelySemisimple	Module.End.maxGenEigenspace Module.End.eigenspace	—	genEigenspace_eq_eigenspace ENat.top_pos

Module.End.IsSemisimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_iff_forall_eigenvalue 📖	mathematical	—	Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Submodule.ne_bot_iff smul_eq_zero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero Module.End.mem_eigenspace_iff iSup_eigenspace_eq_top le_antisymm le_iSup iSup_le eq_or_ne le_refl Iff.not Module.End.hasEigenvalue_iff Module.End.eigenspace_zero LinearMap.ker_eq_top
iSup_eigenspace_eq_top 📖	mathematical	—	iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.eigenspace Top.top Submodule.instTop	—	Module.End.IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace Module.End.isFinitelySemisimple_iff_isSemisimple Module.End.iSup_maxGenEigenspace_eq_top

---

← Back to Index