Basic

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

Statistics

Metric	Count
Definitions Eigenvalues, val, HasEigenvalue, HasEigenvector, HasGenEigenvalue, HasGenEigenvector, HasUnifEigenvalue, HasUnifEigenvector, UnifEigenvalues, instCoeOut, val, instDecidableEq, eigenspace, genEigenrange, genEigenspace, maxGenEigenspace, maxGenEigenspaceIndex, maxUnifEigenspaceIndex	18
Theorems mk_val, val_mk, exists_hasEigenvector, isNilpotent_of_isNilpotent, mem_spectrum, of_mem_spectrum, pow, apply_eq_smul, pow_apply, exists_hasUnifEigenvector, exp_ne_zero, isNilpotent_of_isNilpotent, le, lt, mem_spectrum, of_mem_spectrum, pow, apply_eq_smul, hasUnifEigenvalue, pow_apply, mk_val, val_mk, disjoint_genEigenspace, eigenspace_def, eigenspace_div, eigenspace_le_genEigenspace, eigenspace_le_maxGenEigenspace, eigenspace_restrict_eq_bot, eigenspace_restrict_le_eigenspace, eigenspace_zero, eigenspaces_iSupIndep, eigenvectors_linearIndependent, eigenvectors_linearIndependent', exp_ne_zero_of_hasGenEigenvalue, genEigenrange_nat, genEigenspace_directed, genEigenspace_div, genEigenspace_eq_genEigenspace_finrank_of_le, genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, genEigenspace_eq_iSup_genEigenspace_nat, genEigenspace_inf_le_add, genEigenspace_le_genEigenspace_finrank, genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, genEigenspace_le_maximal, genEigenspace_le_smul, genEigenspace_nat, genEigenspace_one, genEigenspace_restrict, genEigenspace_top, genEigenspace_top_eq_maxUnifEigenspaceIndex, genEigenspace_zero, genEigenspace_zero_nat, generalized_eigenvec_disjoint_range_ker, hasEigenvalue_iff, hasEigenvalue_iff_mem_spectrum, hasEigenvalue_of_hasEigenvector, hasEigenvalue_of_hasGenEigenvalue, hasEigenvector_iff, hasGenEigenvalue_iff, hasGenEigenvalue_iff_hasEigenvalue, hasGenEigenvalue_of_hasEigenvalue, hasGenEigenvalue_of_hasGenEigenvalue_of_le, hasGenEigenvector_iff, hasUnifEigenvalue_iff_hasUnifEigenvalue_one, hasUnifEigenvalue_iff_mem_spectrum, iSup_genEigenspace_eq, independent_genEigenspace, independent_maxGenEigenspace, injOn_genEigenspace, injOn_maxGenEigenspace, isNilpotent_restrict_genEigenspace_nat, isNilpotent_restrict_genEigenspace_top, isNilpotent_restrict_maxGenEigenspace_sub_algebraMap, isNilpotent_restrict_sub_algebraMap, map_add_of_iInf_genEigenspace_ne_bot_of_commute, map_genEigenrange_le, map_smul_of_iInf_genEigenspace_ne_bot, mapsTo_genEigenspace_of_comm, mapsTo_maxGenEigenspace_of_comm, mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo, maxGenEigenspace_eq, maxGenEigenspace_eq_genEigenspace_finrank, maxGenEigenspace_eq_maxGenEigenspace_zero, maxUnifEigenspaceIndex_le_finrank, mem_eigenspace_iff, mem_genEigenspace, mem_genEigenspace_nat, mem_genEigenspace_one, mem_genEigenspace_top, mem_genEigenspace_zero, mem_maxGenEigenspace, pos_finrank_genEigenspace_of_hasEigenvalue, inf_genEigenspace	93
Total	111

Module.End

Definitions

Name	Category	Theorems
Eigenvalues 📖	CompOp	7 math math: LinearMap.IsSymmetric.diagonalization_apply_self_apply, LinearMap.IsSymmetric.directSum_decompose_apply, LinearMap.IsSymmetric.diagonalization_symm_apply, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', LinearMap.IsSymmetric.direct_sum_isInternal, LinearMap.IsSymmetric.eigenvectorBasis_def
HasEigenvalue 📖	MathDef	20 math math: hasEigenvalue_iff, exists_eigenvalue, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, hasEigenvalue_iff_isRoot_charpoly, hasEigenvalue_of_hasEigenvector, hasGenEigenvalue_iff_hasEigenvalue, LinearMap.IsSymmetric.hasEigenvalue_eigenvalues, exists_hasEigenvalue_of_genEigenspace_eq_top, LinearMap.hasEigenvalue_zero_tfae, finite_hasEigenvalue, LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional, hasEigenvalue_iff_isRoot, hasEigenvalue_of_isRoot, hasEigenvalue_toLin'_diagonal_iff, HasEigenvalue.of_mem_spectrum, hasEigenvalue_of_hasGenEigenvalue, hasEigenvalue_iff_mem_spectrum, LinearMap.not_hasEigenvalue_zero_tfae, LieModule.Weight.hasEigenvalueAt, hasEigenvalue_toLin_diagonal_iff
HasEigenvector 📖	MathDef	8 math math: IsSelfAdjoint.hasEigenvector_of_isMaxOn, hasEigenvector_toLin'_diagonal, hasEigenvector_iff, IsSelfAdjoint.hasEigenvector_of_isMinOn, IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn, HasEigenvalue.exists_hasEigenvector, LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis, hasEigenvector_toLin_diagonal
HasGenEigenvalue 📖	MathDef	3 math math: hasGenEigenvalue_iff, hasGenEigenvalue_iff_hasEigenvalue, hasGenEigenvalue_of_hasEigenvalue
HasGenEigenvector 📖	MathDef	1 math math: hasGenEigenvector_iff
HasUnifEigenvalue 📖	MathDef	7 math math: hasUnifEigenvalue_iff_mem_spectrum, Eigenvalues.mk_val, UnifEigenvalues.mk_val, HasUnifEigenvector.hasUnifEigenvalue, HasUnifEigenvalue.of_mem_spectrum, Eigenvalues.val_mk, hasUnifEigenvalue_iff_hasUnifEigenvalue_one
HasUnifEigenvector 📖	MathDef	1 math math: HasUnifEigenvalue.exists_hasUnifEigenvector
UnifEigenvalues 📖	CompOp	—
eigenspace 📖	CompOp	36 math math: Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, LinearMap.IsSymmetric.diagonalization_apply_self_apply, eigenspaces_iSupIndep, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, eigenspace_restrict_le_eigenspace, LinearMap.IsSymmetric.directSum_decompose_apply, mem_eigenspace_intrinsicStar_iff, LinearMap.IsSymmetric.card_filter_eigenvalues_eq, LinearMap.IsSymmetric.diagonalization_symm_apply, eigenspace_le_genEigenspace, LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', hasEigenvector_iff, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, LinearMap.IsSymmetric.directSum_isInternal_of_commute, eigenspace_def, LinearMap.IsSymmetric.direct_sum_isInternal, mem_eigenspace_iff, LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute, eigenspace_div, eigenspace_le_maxGenEigenspace, eigenspace_zero, IsFinitelySemisimple.genEigenspace_eq_eigenspace, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, LinearMap.IsSymmetric.LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute, Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace, LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute, LinearMap.finrank_eigenspace_le, eigenspace_aeval_polynomial_degree_1, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces, IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace, LinearMap.IsSymmetric.eigenvectorBasis_def
genEigenrange 📖	CompOp	3 math math: map_genEigenrange_le, genEigenrange_nat, generalized_eigenvec_disjoint_range_ker
genEigenspace 📖	CompOp	37 math math: independent_genEigenspace, genEigenspace_directed, maxGenEigenspace_eq, maxGenEigenspace_eq_genEigenspace_finrank, mapsTo_genEigenspace_of_comm, Submodule.inf_genEigenspace, genEigenspace_top_eq_maxUnifEigenspaceIndex, LinearMap.finrank_genEigenspace_le, iSup_genEigenspace_eq, genEigenspace_inf_le_add, eigenspace_le_genEigenspace, disjoint_genEigenspace, Submodule.inf_iSup_genEigenspace, genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, mem_genEigenspace_top, injOn_genEigenspace, genEigenspace_one, genEigenspace_eq_iSup_genEigenspace_nat, genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, genEigenspace_zero_nat, genEigenspace_top, generalized_eigenvec_disjoint_range_ker, mem_genEigenspace_one, IsFinitelySemisimple.genEigenspace_eq_eigenspace, genEigenspace_div, genEigenspace_eq_genEigenspace_finrank_of_le, genEigenspace_nat, genEigenspace_le_maximal, mem_genEigenspace_nat, hasGenEigenvector_iff, mem_genEigenspace_zero, genEigenspace_le_genEigenspace_finrank, mem_genEigenspace, genEigenspace_zero, genEigenspace_le_smul, genEigenspace_restrict, pos_finrank_genEigenspace_of_hasEigenvalue
maxGenEigenspace 📖	CompOp	24 math math: maxGenEigenspace_eq, maxGenEigenspace_eq_genEigenspace_finrank, maxGenEigenspace_eq_maxGenEigenspace_zero, LieModule.weight_vector_multiplication, iSup_genEigenspace_eq, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, disjoint_iInf_maxGenEigenspace, injOn_maxGenEigenspace, mem_iInf_maxGenEigenspace_iff, LinearMap.finrank_maxGenEigenspace, eigenspace_le_maxGenEigenspace, mapsTo_maxGenEigenspace_of_comm, independent_maxGenEigenspace, mem_maxGenEigenspace, LieModule.maxGenEigenSpace_toEnd_eq_top, Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo, LinearMap.finrank_maxGenEigenspace_zero_eq, genEigenspace_le_maximal, iSup_maxGenEigenspace_eq_top, Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace, LinearMap.finrank_maxGenEigenspace_eq, Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace, IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace, injOn_iInf_maxGenEigenspace
maxGenEigenspaceIndex 📖	CompOp	1 math math: maxGenEigenspace_eq
maxUnifEigenspaceIndex 📖	CompOp	3 math math: genEigenspace_top_eq_maxUnifEigenspaceIndex, maxUnifEigenspaceIndex_le_finrank, genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_genEigenspace 📖	mathematical	—	Disjoint Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder Submodule.instOrderBot DFunLike.coe OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderHom.instFunLike genEigenspace	—	genEigenspace_eq_iSup_genEigenspace_nat Directed.disjoint_iSup_left Submodule.instIsCompactlyGenerated genEigenspace_directed Directed.disjoint_iSup_right Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton disjoint_iff Submodule.nontrivial_iff_ne_bot smulCommClass_self IsScalarTower.left Set.MapsTo.inter_inter mapsTo_genEigenspace_of_comm Algebra.mul_sub_algebraMap_commutes Commute.isNilpotent_sub LinearMap.ext map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass smul_sub sub_sub add_sub_left_comm SMulCommClass.smul_comm isNilpotent_restrict_of_le inf_le_right isNilpotent_restrict_genEigenspace_nat inf_le_left Submodule.isScalarTower' sub_sub_sub_cancel_left RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass sub_eq_zero isNilpotent_iff_eq_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors IsNilpotent.map_iff RingHomClass.toMonoidWithZeroHomClass FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero instNontrivial LinearMap.instIsTorsionFree Ideal.instIsTorsionFreeSubtypeMemSubmodule
eigenspace_def 📖	mathematical	—	eigenspace LinearMap.ker CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring Module.End LinearMap LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne	—	smulCommClass_self eigenspace.eq_1 genEigenspace_one
eigenspace_div 📖	mathematical	—	eigenspace EuclideanDomain.toCommRing Field.toEuclideanDomain DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing LinearMap.ker DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring Module.End LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing DFunLike.coe RingHom CommSemiring.toSemiring Semifield.toCommSemiring instSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.toSMul Algebra.id IsScalarTower.left	—	genEigenspace_div
eigenspace_le_genEigenspace 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder eigenspace DFunLike.coe OrderHom ENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderHom.instFunLike genEigenspace ENat.instNatCast	—	OrderHom.monotone IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass zero_add
eigenspace_le_maxGenEigenspace 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder eigenspace maxGenEigenspace	—	OrderHom.monotone OrderTop.le_top
eigenspace_restrict_eq_bot 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Disjoint Submodule.instPartialOrder Submodule.instOrderBot eigenspace	Submodule.addCommGroup CommRing.toRing Submodule.module LinearMap.restrict Bot.bot Submodule.instBot	—	eq_bot_iff AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Disjoint.le_bot eigenspace_restrict_le_eigenspace Subtype.prop
eigenspace_restrict_le_eigenspace 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring	Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.map Submodule.addCommMonoid Submodule.module RingHomSurjective.ids Submodule.subtype eigenspace Submodule.addCommGroup CommRing.toRing LinearMap.restrict	—	RingHomSurjective.ids
eigenspace_zero 📖	mathematical	—	eigenspace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap.ker CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring	—	Nat.cast_one genEigenspace_zero_nat pow_one
eigenspaces_iSupIndep 📖	mathematical	—	iSupIndep Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice eigenspace	—	independent_genEigenspace
eigenvectors_linearIndependent 📖	mathematical	HasEigenvector Set Set.instMembership	LinearIndependent Set.Elem CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	eigenvectors_linearIndependent' Subtype.coe_injective
eigenvectors_linearIndependent' 📖	mathematical	HasEigenvector	LinearIndependent CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	iSupIndep.linearIndependent iSupIndep.comp eigenspaces_iSupIndep
exp_ne_zero_of_hasGenEigenvalue 📖	—	HasGenEigenvalue	—	—	HasUnifEigenvalue.exp_ne_zero
genEigenrange_nat 📖	mathematical	—	genEigenrange ENat ENat.instNatCast LinearMap.range CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Module.End LinearMap Monoid.toNatPow instMonoid LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne	—	Submodule.ext RingHomSurjective.ids smulCommClass_self iInf_congr_Prop IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass le_rfl pow_add
genEigenspace_directed 📖	mathematical	—	Directed Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat ENat.instNatCast Submodule.instPartialOrder DFunLike.coe OrderHom OrderHom.instFunLike genEigenspace	—	IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass Monotone.directed_le SemilatticeSup.instIsDirectedOrder Monotone.comp OrderHom.monotone
genEigenspace_div 📖	mathematical	—	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat LinearMap.ker DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Module.End LinearMap LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne	—	smulCommClass_self div_eq_mul_inv mul_comm genEigenspace_one smul_smul LinearMap.ker_smul smul_sub smul_inv_smul₀
genEigenspace_eq_genEigenspace_finrank_of_le 📖	mathematical	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace ENat.instNatCast	—	le_antisymm genEigenspace_le_genEigenspace_finrank OrderHom.monotone IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le 📖	mathematical	maxUnifEigenspaceIndex	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace ENat.instNatCast	—	le_antisymm genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex OrderHom.monotone IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
genEigenspace_eq_iSup_genEigenspace_nat 📖	mathematical	—	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace iSup Preorder.toLE ENat.instNatCast ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	smulCommClass_self genEigenspace_nat iSup_subtype iSup_congr_Prop
genEigenspace_inf_le_add 📖	mathematical	Commute Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instMul	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instMin DFunLike.coe OrderHom ENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderHom.instFunLike genEigenspace LinearMap.instAdd RingHom.id Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonAssocSemiring.toNonUnitalNonAssocSemiring instCommSemiringENat	—	smulCommClass_self add_smul add_sub_add_comm Commute.sub_left IsScalarTower.left Commute.sub_right Algebra.commute_algebraMap_right Algebra.commute_algebraMap_left Commute.add_pow' LinearMap.coe_sum Finset.sum_apply Nat.cast_add add_le_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.sum_eq_zero Finset.HasAntidiagonal.mem_antidiagonal Commute.eq Commute.pow_pow mul_apply pow_map_zero_of_le map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass AddMonoid.nat_smulCommClass' LinearMap.smul_apply smul_zero
genEigenspace_le_genEigenspace_finrank 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder DFunLike.coe OrderHom ENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderHom.instFunLike genEigenspace ENat.instNatCast Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	OrderHom.monotone le_top genEigenspace_top_eq_maxUnifEigenspaceIndex isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass maxUnifEigenspaceIndex_le_finrank
genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder DFunLike.coe OrderHom ENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderHom.instFunLike genEigenspace ENat.instNatCast maxUnifEigenspaceIndex	—	genEigenspace_top_eq_maxUnifEigenspaceIndex OrderHom.monotone le_top
genEigenspace_le_maximal 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder DFunLike.coe OrderHom ENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderHom.instFunLike genEigenspace ENat.instNatCast maxGenEigenspace	—	OrderHom.monotone le_top
genEigenspace_le_smul 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder DFunLike.coe OrderHom ENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderHom.instFunLike genEigenspace Module.End LinearMap.instSMul RingHom.id Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	smulCommClass_self SemigroupAction.mul_smul smul_sub smul_pow IsScalarTower.right IsScalarTower.left Algebra.to_smulCommClass LinearMap.smul_apply smul_zero
genEigenspace_nat 📖	mathematical	—	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace ENat.instNatCast LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Module.End LinearMap Monoid.toNatPow instMonoid LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne	—	Submodule.ext smulCommClass_self
genEigenspace_one 📖	mathematical	—	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat LinearMap.ker RingHom.id Module.End LinearMap LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne	—	smulCommClass_self Nat.cast_one genEigenspace_nat pow_one
genEigenspace_restrict 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring	OrderHom ENat Submodule.addCommGroup CommRing.toRing Submodule.module PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace LinearMap.restrict Submodule.comap Submodule.addCommMonoid Submodule.subtype	—	Submodule.ext smulCommClass_self RingHomCompTriple.ids genEigenspace_nat pow_zero one_eq_id Submodule.ker_subtype pow_succ LinearMap.ker_comp LinearMap.comp_assoc mem_genEigenspace
genEigenspace_top 📖	mathematical	—	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace Top.top instTopENat iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice ENat.instNatCast	—	genEigenspace_eq_iSup_genEigenspace_nat iSup_subtype iSup_congr_Prop iSup_pos
genEigenspace_top_eq_maxUnifEigenspaceIndex 📖	mathematical	—	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace Top.top instTopENat ENat.instNatCast maxUnifEigenspaceIndex	—	WellFoundedGT.iSup_eq_monotonicSequenceLimit wellFoundedGT iSup_congr_Prop iSup_pos iSup_prod' iSup_subtype' sSup_range Set.ext le_refl
genEigenspace_zero 📖	mathematical	—	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace instZeroENat Bot.bot Submodule.instBot	—	Submodule.ext mem_genEigenspace_zero
genEigenspace_zero_nat 📖	mathematical	—	DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ENat.instNatCast LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Module.End Monoid.toNatPow instMonoid	—	Submodule.ext smulCommClass_self zero_smul sub_zero
generalized_eigenvec_disjoint_range_ker 📖	mathematical	—	Disjoint Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid Submodule.instPartialOrder Submodule.instOrderBot genEigenrange ENat ENat.instNatCast Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderHom.instFunLike genEigenspace	—	smulCommClass_self IsScalarTower.left genEigenspace_nat RingHomCompTriple.ids LinearMap.ker_comp genEigenspace_eq_genEigenspace_finrank_of_le disjoint_iff_inf_le RingHomSurjective.ids genEigenrange_nat LinearMap.range_eq_map Submodule.map_inf_eq_map_inf_comap top_inf_eq Submodule.map_comap_le
hasEigenvalue_iff 📖	mathematical	—	HasEigenvalue	—	—
hasEigenvalue_iff_mem_spectrum 📖	mathematical	—	HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain Set Set.instMembership spectrum Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Semifield.toCommSemiring instRing instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	hasUnifEigenvalue_iff_mem_spectrum
hasEigenvalue_of_hasEigenvector 📖	mathematical	HasEigenvector	HasEigenvalue	—	HasUnifEigenvector.hasUnifEigenvalue
hasEigenvalue_of_hasGenEigenvalue 📖	mathematical	HasGenEigenvalue	HasEigenvalue	—	HasUnifEigenvalue.lt zero_lt_one IsOrderedRing.toZeroLEOneClass NeZero.charZero_one
hasEigenvector_iff 📖	mathematical	—	HasEigenvector Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike eigenspace	—	—
hasGenEigenvalue_iff 📖	mathematical	—	HasGenEigenvalue	—	—
hasGenEigenvalue_iff_hasEigenvalue 📖	mathematical	—	HasGenEigenvalue HasEigenvalue	—	IsOrderedRing.toZeroLEOneClass NeZero.charZero_one
hasGenEigenvalue_of_hasEigenvalue 📖	mathematical	HasEigenvalue	HasGenEigenvalue	—	HasUnifEigenvalue.lt
hasGenEigenvalue_of_hasGenEigenvalue_of_le 📖	—	HasGenEigenvalue	—	—	HasUnifEigenvalue.le IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
hasGenEigenvector_iff 📖	mathematical	—	HasGenEigenvector 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 ENat.instNatCast	—	—
hasUnifEigenvalue_iff_hasUnifEigenvalue_one 📖	mathematical	ENat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat instZeroENat	HasUnifEigenvalue AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	HasUnifEigenvalue.lt zero_lt_one IsOrderedRing.toZeroLEOneClass NeZero.charZero_one
hasUnifEigenvalue_iff_mem_spectrum 📖	mathematical	—	HasUnifEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set Set.instMembership spectrum Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Semifield.toCommSemiring instRing 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	—	smulCommClass_self IsScalarTower.left spectrum.mem_iff IsUnit.sub_iff LinearMap.isUnit_iff_ker_eq_bot HasUnifEigenvalue.eq_1 genEigenspace_one not_iff_not
iSup_genEigenspace_eq 📖	mathematical	—	iSup Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice DFunLike.coe OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace ENat.instNatCast maxGenEigenspace	—	genEigenspace_top
independent_genEigenspace 📖	mathematical	—	iSupIndep Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice DFunLike.coe OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace	—	Finset.induction_on Finset.sup_empty Finset.mem_insert Finset.sup_insert disjoint_iff Submodule.eq_bot_iff Submodule.mem_sup smulCommClass_self mapsTo_genEigenspace_of_comm Algebra.mul_sub_algebraMap_pow_commutes IsScalarTower.left SetLike.mem_coe map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass zero_add RingHomSurjective.ids Submodule.map.congr_simp Finset.sup_eq_iSup Submodule.map_iSup iSup₂_mono Submodule.mem_map_of_mem Submodule.mem_bot Disjoint.eq_bot disjoint_genEigenspace iSupIndep_iff_supIndep_of_injOn Submodule.instIsCompactlyGenerated injOn_genEigenspace Finset.notMem_erase
independent_maxGenEigenspace 📖	mathematical	—	iSupIndep Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice maxGenEigenspace	—	independent_genEigenspace
injOn_genEigenspace 📖	mathematical	—	Set.InjOn Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace setOf Bot.bot Submodule.instBot	—	disjoint_genEigenspace
injOn_maxGenEigenspace 📖	mathematical	—	Set.InjOn Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid maxGenEigenspace setOf Bot.bot Submodule.instBot	—	injOn_genEigenspace
isNilpotent_restrict_genEigenspace_nat 📖	mathematical	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne SetLike.coe Submodule Submodule.setLike OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace ENat.instNatCast mapsTo_genEigenspace_of_comm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instRing RingHom RingHom.instFunLike algebraMap instAlgebra Algebra.toSMul Algebra.id IsScalarTower.left Algebra.mul_sub_algebraMap_commutes	IsNilpotent LinearMap SetLike.instMembership Submodule.addCommMonoid Submodule.module LinearMap.instZero Monoid.toNatPow instMonoid LinearMap.restrict	—	smulCommClass_self LinearMap.ext LinearMap.zero_apply AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass ZeroMemClass.coe_zero ZeroMemClass.coe_eq_zero pow_apply_mem_of_forall_mem pow_restrict LinearMap.restrict_apply mem_genEigenspace_nat
isNilpotent_restrict_genEigenspace_top 📖	mathematical	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne SetLike.coe Submodule Submodule.setLike OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace Top.top instTopENat mapsTo_genEigenspace_of_comm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instRing RingHom RingHom.instFunLike algebraMap instAlgebra Algebra.toSMul Algebra.id IsScalarTower.left Algebra.mul_sub_algebraMap_commutes	IsNilpotent LinearMap SetLike.instMembership Submodule.addCommMonoid Submodule.module LinearMap.instZero Monoid.toNatPow instMonoid LinearMap.restrict	—	smulCommClass_self isNilpotent_restrict_of_le mapsTo_genEigenspace_of_comm IsScalarTower.left Algebra.mul_sub_algebraMap_commutes genEigenspace_top_eq_maxUnifEigenspaceIndex le_refl isNilpotent_restrict_genEigenspace_nat
isNilpotent_restrict_maxGenEigenspace_sub_algebraMap 📖	mathematical	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LinearMap.instSub RingHom instSemiring RingHom.instFunLike algebraMap 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 SetLike.coe Submodule Submodule.setLike maxGenEigenspace mapsTo_maxGenEigenspace_of_comm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instRing Algebra.mul_sub_algebraMap_commutes	IsNilpotent LinearMap SetLike.instMembership Submodule.addCommMonoid Submodule.module LinearMap.instZero Monoid.toNatPow instMonoid LinearMap.restrict	—	smulCommClass_self IsScalarTower.left isNilpotent_restrict_of_le mapsTo_genEigenspace_of_comm Algebra.mul_sub_algebraMap_commutes maxGenEigenspace_eq le_refl isNilpotent_restrict_genEigenspace_nat
isNilpotent_restrict_sub_algebraMap 📖	mathematical	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring LinearMap.instSub RingHom instSemiring RingHom.instFunLike algebraMap 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 SetLike.coe Submodule Submodule.setLike OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace ENat.instNatCast mapsTo_genEigenspace_of_comm SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instRing Algebra.mul_sub_algebraMap_commutes	IsNilpotent LinearMap SetLike.instMembership Submodule.addCommMonoid Submodule.module LinearMap.instZero Monoid.toNatPow instMonoid LinearMap.restrict	—	smulCommClass_self IsScalarTower.left isNilpotent_restrict_genEigenspace_nat mapsTo_genEigenspace_of_comm Algebra.mul_sub_algebraMap_commutes
map_add_of_iInf_genEigenspace_ne_bot_of_commute 📖	mathematical	Commute Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instMul DFunLike.coe	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	le_inf_iff iInf_le eq_bot_iff le_trans disjoint_iff_inf_le Disjoint.mono_left genEigenspace_inf_le_add map_add disjoint_genEigenspace
map_genEigenrange_le 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids genEigenrange EuclideanDomain.toCommRing Field.toEuclideanDomain ENat ENat.instNatCast	—	RingHomSurjective.ids smulCommClass_self IsScalarTower.left genEigenrange_nat LinearMap.range_comp Algebra.mul_sub_algebraMap_pow_commutes LinearMap.map_le_range
map_smul_of_iInf_genEigenspace_ne_bot 📖	mathematical	—	Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	smulCommClass_self le_inf_iff iInf_le eq_bot_iff le_trans disjoint_iff_inf_le Disjoint.mono_left genEigenspace_le_smul map_smul disjoint_genEigenspace
mapsTo_genEigenspace_of_comm 📖	mathematical	Commute Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instMul	Set.MapsTo DFunLike.coe LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule Submodule.setLike OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace	—	smulCommClass_self Commute.pow_left IsScalarTower.left Commute.sub_left Algebra.commute_algebraMap_left RingHomCompTriple.ids LinearMap.comp_apply mul_eq_comp Commute.eq map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
mapsTo_maxGenEigenspace_of_comm 📖	mathematical	Commute Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instMul	Set.MapsTo DFunLike.coe LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule Submodule.setLike maxGenEigenspace	—	mapsTo_genEigenspace_of_comm
mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo 📖	mathematical	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule Submodule.setLike maxGenEigenspace	SetLike.instMembership LinearMap Submodule.addCommMonoid Submodule.module LinearMap.restrict Submodule.addCommGroup CommRing.toRing	—	smulCommClass_self Submodule.smul_mem LinearMap.restrict_smul_one Submodule.sub_mem LinearMap.restrict_sub pow_apply_mem_of_forall_mem pow_restrict
maxGenEigenspace_eq 📖	mathematical	—	maxGenEigenspace DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace ENat.instNatCast maxGenEigenspaceIndex	—	genEigenspace_top_eq_maxUnifEigenspaceIndex
maxGenEigenspace_eq_genEigenspace_finrank 📖	mathematical	—	maxGenEigenspace EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe OrderHom ENat Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike genEigenspace ENat.instNatCast Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	le_antisymm genEigenspace_top_eq_maxUnifEigenspaceIndex isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain genEigenspace_le_genEigenspace_finrank OrderHom.monotone le_top
maxGenEigenspace_eq_maxGenEigenspace_zero 📖	mathematical	—	maxGenEigenspace Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instSub RingHom.id Semiring.toNonAssocSemiring LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Submodule.ext smulCommClass_self zero_smul sub_zero
maxUnifEigenspaceIndex_le_finrank 📖	mathematical	—	maxUnifEigenspaceIndex EuclideanDomain.toCommRing Field.toEuclideanDomain Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	—	Nat.sInf_le le_antisymm OrderHom.monotone OrderEmbedding.monotone smulCommClass_self genEigenspace_nat ker_pow_le_ker_pow_finrank
mem_eigenspace_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike eigenspace DFunLike.coe Module.End 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	—	mem_genEigenspace_one
mem_genEigenspace 📖	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 Preorder.toLE ENat.instNatCast LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Module.End LinearMap Monoid.toNatPow instMonoid LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne	—	zero_le smulCommClass_self Monotone.directed_le SemilatticeSup.instIsDirectedOrder OrderHom.monotone iSup_subtype' Submodule.mem_iSup_of_directed
mem_genEigenspace_nat 📖	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 ENat.instNatCast LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Module.End LinearMap Monoid.toNatPow instMonoid LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne	—	smulCommClass_self mem_genEigenspace OrderHom.monotone IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass le_rfl
mem_genEigenspace_one 📖	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 AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat Module.End LinearMap.instFunLike RingHom.id 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 genEigenspace_one LinearMap.mem_ker LinearMap.sub_apply sub_eq_zero LinearMap.smul_apply one_apply
mem_genEigenspace_top 📖	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 Top.top instTopENat LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Module.End LinearMap Monoid.toNatPow instMonoid LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne	—	smulCommClass_self
mem_genEigenspace_zero 📖	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 instZeroENat NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Nat.cast_zero smulCommClass_self mem_genEigenspace_nat pow_zero LinearMap.mem_ker one_apply
mem_maxGenEigenspace 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike maxGenEigenspace DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow instMonoid LinearMap.instSub LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instOne NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mem_genEigenspace_top
pos_finrank_genEigenspace_of_hasEigenvalue 📖	mathematical	HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain	Module.finrank 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 ENat.instNatCast DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.addCommMonoid Submodule.module	—	finrank_bot EuclideanDomain.toNontrivial Submodule.finrank_lt_finrank_of_lt FiniteDimensional.finiteDimensional_submodule bot_lt_iff_ne_bot Submodule.finrank_mono IsNoetherianRing.strongRankCondition PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain OrderHom.monotone IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass zero_add

Module.End.Eigenvalues

Definitions

Name	Category	Theorems
val 📖	CompOp	2 math math: mk_val, val_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_val 📖	mathematical	—	Module.End.HasUnifEigenvalue ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat val	—	—
val_mk 📖	mathematical	Module.End.HasEigenvalue	val Module.End.HasUnifEigenvalue ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	—

Module.End.HasEigenvalue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_hasEigenvector 📖	mathematical	Module.End.HasEigenvalue	Module.End.HasEigenvector	—	Submodule.exists_mem_ne_zero_of_ne_bot
isNilpotent_of_isNilpotent 📖	mathematical	IsNilpotent Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid Module.End.HasEigenvalue	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Module.End.HasUnifEigenvalue.isNilpotent_of_isNilpotent
mem_spectrum 📖	mathematical	Module.End.HasEigenvalue	Set Set.instMembership spectrum Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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	—	Module.End.HasUnifEigenvalue.mem_spectrum
of_mem_spectrum 📖	mathematical	Set Set.instMembership spectrum Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Semifield.toCommSemiring Module.End.instRing Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Module.End.HasEigenvalue	—	smulCommClass_self IsScalarTower.left Module.End.hasEigenvalue_iff_mem_spectrum
pow 📖	mathematical	Module.End.HasEigenvalue	Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Monoid.toNatPow Module.End.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Module.End.HasUnifEigenvalue.pow

Module.End.HasEigenvector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_smul 📖	mathematical	Module.End.HasEigenvector	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	—	Module.End.HasUnifEigenvector.apply_eq_smul
pow_apply 📖	mathematical	Module.End.HasEigenvector	DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Module.End.HasUnifEigenvector.pow_apply

Module.End.HasUnifEigenvalue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_hasUnifEigenvector 📖	mathematical	Module.End.HasUnifEigenvalue	Module.End.HasUnifEigenvector	—	Submodule.exists_mem_ne_zero_of_ne_bot
exp_ne_zero 📖	—	Module.End.HasUnifEigenvalue ENat ENat.instNatCast	—	—	Nat.cast_zero Module.End.genEigenspace_zero
isNilpotent_of_isNilpotent 📖	mathematical	IsNilpotent Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid Module.End.HasUnifEigenvalue ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCommSemiringENat	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	exists_hasUnifEigenvector isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors IsDomain.toNontrivial IsDomain.toIsCancelMulZero Module.End.HasUnifEigenvector.pow_apply
le 📖	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Module.End.HasUnifEigenvalue	—	—	Mathlib.Tactic.Contrapose.contrapose₄ le_bot_iff OrderHom.monotone
lt 📖	—	ENat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat instZeroENat Module.End.HasUnifEigenvalue	—	—	le Order.one_le_iff_pos IsOrderedRing.toZeroLEOneClass NeZero.charZero_one eq_bot_iff smulCommClass_self Module.End.mem_genEigenspace LinearMap.ker_eq_bot Module.End.coe_pow Function.Injective.iterate Module.End.genEigenspace_one
mem_spectrum 📖	mathematical	Module.End.HasUnifEigenvalue ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Set Set.instMembership spectrum Module.End CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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	—	smulCommClass_self IsScalarTower.left spectrum.mem_iff RingHomInvPair.ids exists_hasUnifEigenvector LinearMap.ker_eq_bot' LinearEquiv.ker Module.End.HasUnifEigenvector.apply_eq_smul sub_self
of_mem_spectrum 📖	mathematical	Set Set.instMembership spectrum Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Semifield.toCommSemiring Module.End.instRing Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Module.End.HasUnifEigenvalue ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	smulCommClass_self IsScalarTower.left Module.End.hasUnifEigenvalue_iff_mem_spectrum
pow 📖	mathematical	Module.End.HasUnifEigenvalue ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	Module.End CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Monoid.toNatPow Module.End.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eq_1 Submodule.ne_bot_iff exists_hasUnifEigenvector Module.End.HasUnifEigenvector.pow_apply

Module.End.HasUnifEigenvector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_smul 📖	mathematical	Module.End.HasUnifEigenvector ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	DFunLike.coe Module.End CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Module.End.mem_genEigenspace_one
hasUnifEigenvalue 📖	mathematical	Module.End.HasUnifEigenvector	Module.End.HasUnifEigenvalue	—	Module.End.HasUnifEigenvalue.eq_1 Submodule.ne_bot_iff
pow_apply 📖	mathematical	Module.End.HasUnifEigenvector ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	DFunLike.coe Module.End CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Monoid.toNatPow Module.End.instMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	pow_zero one_smul pow_succ apply_eq_smul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass smul_smul pow_succ'

Module.End.UnifEigenvalues

Definitions

Name	Category	Theorems
instCoeOut 📖	CompOp	—
val 📖	CompOp	9 math math: LinearMap.IsSymmetric.diagonalization_apply_self_apply, LinearMap.IsSymmetric.directSum_decompose_apply, LinearMap.IsSymmetric.diagonalization_symm_apply, val_mk, mk_val, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', LinearMap.IsSymmetric.direct_sum_isInternal, LinearMap.IsSymmetric.eigenvectorBasis_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_val 📖	mathematical	—	Module.End.HasUnifEigenvalue val	—	—
val_mk 📖	mathematical	Module.End.HasUnifEigenvalue	val	—	—

Module.End.UnivEigenvalues

Definitions

Name	Category	Theorems
instDecidableEq 📖	CompOp	3 math math: LinearMap.IsSymmetric.directSum_decompose_apply, LinearMap.IsSymmetric.direct_sum_isInternal, LinearMap.IsSymmetric.eigenvectorBasis_def

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf_genEigenspace 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring	instMin OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat instPartialOrder OrderHom.instFunLike Module.End.genEigenspace map addCommMonoid module RingHomSurjective.ids subtype addCommGroup CommRing.toRing LinearMap.restrict	—	RingHomSurjective.ids Module.End.genEigenspace_restrict map_comap_eq range_subtype

---

← Back to Index