Theorems · Definition · linear algebra
Module.End.maxUnifEigenspaceIndex
{R : Type v} →
{M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕIf there exists a natural number k such that the kernel of (f - μ • id) ^ k is the
maximal generalized eigenspace, then this value is the least such k. If not, this value is not
meaningful.
- Defined in
- Mathlib.LinearAlgebra.Eigenspace.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- Module.Endstatement and proof · cited by 774
- Module.End.genEigenspaceproof · cited by 70
- OrderHom.compproof · cited by 61
- OrderEmbedding.toOrderHomproof · cited by 16
- WithTop.coeOrderHomproof · cited by 6
- monotonicSequenceLimitIndexproof · cited by 3
Cited by9
Results whose statement or proof uses this declaration.
- Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndexstatement and proof · cited by 5
- Module.End.maxGenEigenspaceIndexproof · cited by 4
- Module.End.genEigenspace_le_genEigenspace_finrankproof · cited by 2
- Module.End.maxUnifEigenspaceIndex_le_finrankstatement · cited by 1
- Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndexstatement · cited by 1
- Module.End.isNilpotent_restrict_maxGenEigenspace_sub_algebraMapproof · cited by 1
- Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_lestatement and proof · cited by 0
- Module.End.isNilpotent_restrict_genEigenspace_topproof · cited by 0
- Module.End.maxGenEigenspace_eq_genEigenspace_finrankproof · cited by 0