Semisimple

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

Statistics

Metric	Count
Definitions	0
Theorems genEigenspace_eq_eigenspace, maxGenEigenspace_eq_eigenspace, apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil	3
Total	3

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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace Commute Module.End instMul IsFinitelySemisimple IsNilpotent LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow instMonoid LinearMap.instSub	LinearMap.instFunLike 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 Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat instZeroENat	DFunLike.coe OrderHom Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat 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 IsOrderedRing.toZeroLEOneClass NeZero.charZero_one
maxGenEigenspace_eq_eigenspace 📖	mathematical	Module.End.IsFinitelySemisimple	Module.End.maxGenEigenspace Module.End.eigenspace	—	genEigenspace_eq_eigenspace ENat.top_pos

---

← Back to Index