Module.End.maximalGeneralizedEigenspace_eq
theorem Module.End.maximalGeneralizedEigenspace_eq :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[h : IsNoetherian R M] (f : Module.End R M) (μ : R),
f.maximalGeneralizedEigenspace μ = (f.generalizedEigenspace μ) (f.maximalGeneralizedEigenspaceIndex μ)
This theorem states that for a given endomorphism of a Noetherian module, its maximal generalized eigenspace is always of the form `kernel (f - μ • id) ^ k` for some `k`. Here, `R` is the type of the scalars, `M` is the type of the module, `f` is the endomorphism, and `μ` is a scalar. The maximal generalized eigenspace of `f` with respect to `μ` is equal to the generalized eigenspace of `f` with respect to `μ` at the index of the maximal generalized eigenspace of `f` with respect to `μ`. This implies that in the context of Noetherian modules, the size of the largest generalized eigenspace is determined by the power to which `f - μ • id` must be raised to yield the kernel.
More concisely: For any endomorphism of a Noetherian module and scalar, the maximal generalized eigenspace is equal to the kernel of the power of the endomorphism minus the scalar identity, raised to the power of the index of the maximal generalized eigenspace.
|
Module.End.exp_ne_zero_of_hasGeneralizedEigenvalue
theorem Module.End.exp_ne_zero_of_hasGeneralizedEigenvalue :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
{μ : R} {k : ℕ}, f.HasGeneralizedEigenvalue μ k → k ≠ 0
This theorem states that the exponent of a generalized eigenvalue is never zero. In more detail, for any commutative ring `R` and an additive commutative group `M` that forms a module over `R`, and any endomorphism `f` of this module, if `f` has a generalized eigenvalue `μ` with exponent `k`, then `k` cannot be zero. Here, a generalized eigenvalue for `f` with exponent `k` denotes that `(f - μI)^k` annihilates some non-zero vector, where `I` is the identity transformation and 'annihilates' means it sends the vector to zero.
More concisely: For any commutative ring `R`, additive commutative group `M` as an `R`-module, and endomorphism `f` of `M`, if `f` has a generalized eigenvalue `μ` with non-zero exponent `k`, then `k` is not equal to zero.
|
Module.End.generalizedEigenspace_eq_generalizedEigenspace_finrank_of_le
theorem Module.End.generalizedEigenspace_eq_generalizedEigenspace_finrank_of_le :
∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] (f : Module.End K V) (μ : K) {k : ℕ},
FiniteDimensional.finrank K V ≤ k →
(f.generalizedEigenspace μ) k = (f.generalizedEigenspace μ) (FiniteDimensional.finrank K V)
This theorem states that for a given module endomorphism `f` of a finite dimensional vector space `V` over a field `K`, the generalized eigenspace associated with an eigenvalue `μ` and an exponent `k` is equal to the generalized eigenspace associated with `μ` and the rank of `V` over `K` (i.e., the dimension of `V`), provided that `k` is greater than or equal to the rank of `V` over `K`. Essentially, it means that for exponents at least as large as the dimension of the vector space, the generalized eigenspaces are the same.
More concisely: For a finite dimensional vector space endomorphism `f` over field `K` and eigenvalue `μ`, the generalized eigenspaces with exponent `k ≥` the rank of `V` over `K` are equal.
|
Module.End.generalizedEigenspace_restrict
theorem Module.End.generalizedEigenspace_restrict :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
(p : Submodule R M) (k : ℕ) (μ : R) (hfp : ∀ x ∈ p, f x ∈ p),
(Module.End.generalizedEigenspace (LinearMap.restrict f hfp) μ) k =
Submodule.comap p.subtype ((f.generalizedEigenspace μ) k)
This theorem states that if a linear endomorphism `f` maps a subspace `p` of a module `M` over a commutative ring `R` into itself, then the generalized eigenspace of the restriction of `f` to `p` is equivalent to the portion of the generalized eigenspace of `f` that lies within `p`. That is, given a natural number `k` and a ring element `μ`, the kth generalized eigenspace of the restriction of `f` to `p` is exactly the pre-image under the inclusion map of the kth generalized eigenspace of `f` in the whole space `M`. This theorem provides a way to analyze the behavior of linear maps on subspaces by connecting it to their behavior on the whole space.
More concisely: The kth generalized eigenspace of a linear endomorphism's restriction to a subspace is equal to the subspace of the kth generalized eigenspace in the whole space mapped in by the inclusion map.
|
Module.End.generalizedEigenspace_le_generalizedEigenspace_finrank
theorem Module.End.generalizedEigenspace_le_generalizedEigenspace_finrank :
∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] (f : Module.End K V) (μ : K) (k : ℕ),
(f.generalizedEigenspace μ) k ≤ (f.generalizedEigenspace μ) (FiniteDimensional.finrank K V)
This theorem states that for any field `K`, any additive commutative group `V` that is also a module over `K`, and any finite dimensional vector space `V`, for any linear endomorphism `f` from `V` to `V` and any scalar `μ` from `K`, and for any natural number `k`, the generalized eigenspace of `f` corresponding to the eigenvalue `μ` and of order `k` is a subspace of the generalized eigenspace of `f` corresponding to the eigenvalue `μ` and of order equal to the finite dimension of `V` over `K`. This is Lemma 8.11 from Axler's "Linear Algebra Done Right". In other words, every generalized eigenvector of a linear transformation is also a generalized eigenvector of a certain maximum order, specifically the finite dimension of the vector space.
More concisely: For any field `K`, any additive commutative group `V` that is a `K`-module and finite dimensional vector space, and any linear endomorphism `f` from `V` to `V`, `μ` in `K`, and natural number `k`, the generalized eigenspace `E_μ(f, k)` of order `k` is contained in the generalized eigenspace `E_μ(f)` of eigenvalue `μ` of `f`.
|
Module.End.hasGeneralizedEigenvalue_of_hasEigenvalue
theorem Module.End.hasGeneralizedEigenvalue_of_hasEigenvalue :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
{μ : R} {k : ℕ}, 0 < k → f.HasEigenvalue μ → f.HasGeneralizedEigenvalue μ k
This theorem states that all eigenvalues are also generalized eigenvalues. In the context of a commutative ring `R` and an additive commutative group `M`, which is also a module over `R`, for any linear endomorphism `f` of `M`, any eigenvalue `μ` of `f`, and any natural number `k` greater than zero, if `f` has `μ` as an eigenvalue, then `f` also has `μ` as a generalized eigenvalue of order `k`.
More concisely: For any commutative ring `R`, additive commutative group `M` (an `R`-module), linear endomorphism `f` of `M`, eigenvalue `μ` of `f`, and natural number `k` greater than zero, if `μ` is an eigenvalue of `f` then `μ` is also a generalized eigenvalue of `f` of order `k`.
|
Module.End.generalized_eigenvec_disjoint_range_ker
theorem Module.End.generalized_eigenvec_disjoint_range_ker :
∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] (f : Module.End K V) (μ : K),
Disjoint (f.generalizedEigenrange μ (FiniteDimensional.finrank K V))
((f.generalizedEigenspace μ) (FiniteDimensional.finrank K V))
The theorem `Module.End.generalized_eigenvec_disjoint_range_ker` states that for any field `K`, any vector space `V` over `K` that is finite-dimensional, any linear endomorphism `f` of `V`, and any scalar `μ` in `K`, the generalized eigenrange and the generalized eigenspace of `f` corresponding to `μ` for the exponent equal to the rank of `K` over `V` are disjoint. Here, two subsets are said to be disjoint if their intersection is empty, or equivalently, if their infimum is the bottom element.
More concisely: For any field `K`, finite-dimensional vector space `V` over `K`, linear endomorphism `f` of `V`, and scalar `μ` in `K`, the generalized eigenrange and generalized eigenspace of `f` corresponding to `μ` for the exponent equal to the rank of `K` over `V` are empty when intersected.
|
Module.End.eigenspace_le_generalizedEigenspace
theorem Module.End.eigenspace_le_generalizedEigenspace :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
{μ : R} {k : ℕ}, 0 < k → f.eigenspace μ ≤ (f.generalizedEigenspace μ) k
The theorem `Module.End.eigenspace_le_generalizedEigenspace` states that for any commutative ring `R`, any additive commutative group `M`, and any `R`-module structure on `M`, for any endomorphism `f` of the `R`-module `M`, any scalar `μ` from the ring `R`, and any positive integer `k`, the eigenspace of `f` corresponding to `μ` is a subspace of the `k`-th generalized eigenspace of `f` corresponding to `μ`. In simpler terms, this theorem asserts that every eigenspace of a linear transformation is contained within its corresponding generalized eigenspace.
More concisely: For any commutative ring R, additive commutative group M with an R-module structure, endomorphism f of M, scalar μ from R, and positive integer k, the eigenspace of f corresponding to μ is contained in the k-th generalized eigenspace of f corresponding to μ.
|
Module.End.hasGeneralizedEigenvalue_of_hasGeneralizedEigenvalue_of_le
theorem Module.End.hasGeneralizedEigenvalue_of_hasGeneralizedEigenvalue_of_le :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
{μ : R} {k m : ℕ}, k ≤ m → f.HasGeneralizedEigenvalue μ k → f.HasGeneralizedEigenvalue μ m
This theorem states that if a linear endomorphism `f` of a module `M` over a commutative ring `R` has a generalized eigenvalue `μ` for some exponent `k`, then `f` also has a generalized eigenvalue `μ` for any exponent `m` that is greater than or equal to `k`. In other words, if an element `μ` of `R` is a generalized eigenvalue of `f` associated with a certain degree of nilpotency `k`, then `μ` remains a generalized eigenvalue of `f` for all degrees of nilpotency greater than or equal to `k`.
More concisely: If a linear endomorphism of a module over a commutative ring has a generalized eigenvalue for some exponent, then it has that generalized eigenvalue for all greater exponents.
|
Module.End.eigenspaces_independent
theorem Module.End.eigenspaces_independent :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] (f : Module.End R M), CompleteLattice.Independent f.eigenspace
This theorem states that the eigenspaces of a linear operator form an independent set of subspaces within the module `M`. More specifically, it specifies that any given eigenspace has no overlap (i.e., trivial intersection) with the span of all other eigenspaces. The theorem holds for any type `R` with a `CommRing` (commutative ring) structure, any type `M` with an `AddCommGroup` (additive commutative group) structure, a `Module R M` structure (indicating `M` is a module over the ring `R`), and a `NoZeroSMulDivisors R M` condition (indicating that scalar multiplication by a non-zero element of `R` cannot yield the zero element in `M`). The theorem applies to any linear operator `f` from `M` to `M`, asserting the independence of the set of `f`'s eigenspaces.
More concisely: The eigenspaces of a linear operator over a commutative ring form an independent set of subspaces within the module, with no overlap between any given eigenspace and the span of all other eigenspaces.
|
Module.End.eigenvectors_linearIndependent
theorem Module.End.eigenvectors_linearIndependent :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] (f : Module.End R M) (μs : Set R) (xs : ↑μs → M),
(∀ (μ : ↑μs), f.HasEigenvector (↑μ) (xs μ)) → LinearIndependent (ι := ↑μs) R xs
This theorem states that eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly independent. It assumes that we are working with a module `M` over a commutative ring `R`. The linear operator is represented as an endomorphism of the module `M` which is a linear map from `M` to `M`. The set of eigenvalues is denoted by `μs` and for each eigenvalue in `μs`, there is a corresponding eigenvector in `M`, represented by the function `xs` that maps each eigenvalue to its corresponding eigenvector. The condition `f.HasEigenvector (↑μ) (xs μ)` ensures that for each eigenvalue `μ` in `μs`, `xs μ` is indeed an eigenvector of the linear operator `f`. Under these assumptions, the theorem asserts that the vectors `xs μ`, for `μ` in `μs`, are linearly independent.
More concisely: The eigenvectors of a linear operator corresponding to distinct eigenvalues are linearly independent.
|
Module.End.isNilpotent_restrict_sub_algebraMap
theorem Module.End.isNilpotent_restrict_sub_algebraMap :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
(μ : R) (k : ℕ)
(h :
optParam
(Set.MapsTo ⇑(f - (algebraMap R (Module.End R M)) μ) ↑((f.generalizedEigenspace μ) k)
↑((f.generalizedEigenspace μ) k))
⋯),
IsNilpotent (LinearMap.restrict (f - (algebraMap R (Module.End R M)) μ) h)
This theorem states that for any commutative ring `R`, any additive commutative group `M`, and any module `M` over `R`, for any linear endomorphism `f` of `M`, any ring element `μ`, and any natural number `k`, the restriction of the linear map `f - μ • 1` to the k-th generalized μ-eigenspace of `f` is a nilpotent linear map. The k-th generalized μ-eigenspace is the subset of `M` where each element, when transformed by `f`, is mapped into itself scaled by `μ` to the power `k`. A nilpotent linear map is one which, when composed with itself some number of times, results in the zero map.
More concisely: Given a commutative ring `R`, an additive commutative group `M` with a module structure over `R`, an endomorphism `f` of `M`, a ring element `μ`, and a natural number `k`, the restriction of `f - μ • 1` to the `k`-th generalized eigenspace of `f` is a nilpotent linear map.
|
Module.End.eigenspace_restrict_eq_bot
theorem Module.End.eigenspace_restrict_eq_bot :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
{p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) {μ : R},
Disjoint (f.eigenspace μ) p → Module.End.eigenspace (LinearMap.restrict f hfp) μ = ⊥
This theorem states that if an invariant subspace `p` of an endomorphism `f` is disjoint from the `μ`-eigenspace of `f`, then the `μ`-eigenspace of the restriction of `f` to `p` is trivial.
In more mathematical language, given a commutative ring `R`, an additive commutative group `M`, and a module `M` over `R`, if a submodule `p` of `M` is invariant under a linear endomorphism `f` of `M` and is disjoint from the `μ`-eigenspace of `f` (i.e., the set of vectors `x` for which `f x = μ • x`), then the `μ`-eigenspace of the restriction of `f` to `p` is the trivial subspace (denoted `⊥`). This means that the only vector `x` in `p` for which the restriction of `f` satisfies `f x = μ • x` is the zero vector.
More concisely: If a submodule `p` of an `R`-module `M` is invariant under an endomorphism `f` of `M` and is disjoint from the `μ`-eigenspace of `f`, then the `μ`-eigenspace of the restriction of `f` to `p` is the trivial subspace.
|
Module.End.pos_finrank_generalizedEigenspace_of_hasEigenvalue
theorem Module.End.pos_finrank_generalizedEigenspace_of_hasEigenvalue :
∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : FiniteDimensional K V] {f : Module.End K V} {k : ℕ} {μ : K},
f.HasEigenvalue μ → 0 < k → 0 < FiniteDimensional.finrank K ↥((f.generalizedEigenspace μ) k)
This theorem states that for any field `K`, vector space `V` over `K`, endomorphism `f` of `V`, positive integer `k`, and scalar `μ` in `K`, if `f` has `μ` as an eigenvalue, then the dimension (or rank) of the generalized eigenspace of `f` corresponding to `μ` at exponent `k` is positive. In simple terms, if `f` has an eigenvalue `μ`, then the generalized eigenspace related to `μ` at any positive power contains at least one non-zero vector. The dimension of this eigenspace is calculated using the function `FiniteDimensional.finrank`. The generalized eigenspace is a subspace of `V` consisting of vectors that become a zero vector after applying the endomorphism `f` subtracted by `μ` times identity map for `k` times.
More concisely: For any field `K`, vector space `V` over `K`, endomorphism `f` of `V`, positive integer `k`, and scalar `μ` in `K`, if `f` has eigenvalue `μ` then the dimension of the generalized eigenspace of `f` corresponding to `μ` at exponent `k` is positive.
|
Module.End.map_generalizedEigenrange_le
theorem Module.End.map_generalizedEigenrange_le :
∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : Module.End K V}
{μ : K} {n : ℕ}, Submodule.map f (f.generalizedEigenrange μ n) ≤ f.generalizedEigenrange μ n
This theorem states that for any field `K`, any additive commutative group `V`, and any module structure on `V` over `K`, for any endomorphism `f` of this module and any scalar `μ` in `K` and positive natural number `n`, the generalized eigenrange of `f` with eigenvalue `μ` and rank `n`, when mapped under `f`, is a subset of or equal to the original generalized eigenrange. In other words, a linear map maps a generalized eigenrange into itself.
More concisely: For any endomorphism `f` of a `K`-module `V` with module structure over a field `K`, and for any eigenvalue `μ` in `K` and positive natural number `n`, the generalized eigenrange of `f` with eigenvalue `μ` and rank `n` is contained in the image of the generalized eigenrange with eigenvalue `μ` under the map `f`.
|
Module.End.isNilpotent_restrict_iSup_sub_algebraMap
theorem Module.End.isNilpotent_restrict_iSup_sub_algebraMap :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsNoetherian R M] (f : Module.End R M) (μ : R)
(h :
optParam
(Set.MapsTo ⇑(f - (algebraMap R (Module.End R M)) μ) ↑(⨆ k, (f.generalizedEigenspace μ) k)
↑(⨆ k, (f.generalizedEigenspace μ) k))
⋯),
IsNilpotent (LinearMap.restrict (f - (algebraMap R (Module.End R M)) μ) h)
This theorem states that for any commutative ring `R` and any `R`-module `M` that is also a Noetherian module, given an endomorphism `f` of the module `M` and an element `μ` from the ring `R`, the restriction of `(f - μ • 1)` to the generalized `μ`-eigenspace is a nilpotent operator. Here, `(f - μ • 1)` represents the original endomorphism minus `μ` times the identity operator and the generalized `μ`-eigenspace is a direct sum of generalized eigenspaces for the eigenvalue `μ`. An operator is said to be nilpotent if some natural-number-power of it equals zero. The optParam function is used for optional parameters, and Set.MapsTo ensures that the image of the generalized `μ`-eigenspace under `(f - μ • 1)` is contained in the generalized `μ`-eigenspace. The theorem is important in the study of the structure of linear operators on finite-dimensional vector spaces.
More concisely: Given a commutative ring `R`, an `R`-module `M` that is Noetherian, an endomorphism `f` of `M`, and an element `μ` from `R`, the restriction of `(f - μ • 1)` to the generalized `μ`-eigenspace is a nilpotent operator.
|
Module.End.mem_eigenspace_iff
theorem Module.End.mem_eigenspace_iff :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
{μ : R} {x : M}, x ∈ f.eigenspace μ ↔ f x = μ • x
This theorem states that for any commutative ring `R`, an additive commutative group `M`, and a module `M` over the ring `R`, given a linear transformation `f` from `M` to `M`, a scalar `μ` from the ring `R`, and a vector `x` from `M`, `x` is an element of the eigenspace of `f` corresponding to the eigenvalue `μ` if and only if `f` acting on `x` equals `μ` scaled by `x`. In mathematical terms, this states that $x$ is an eigenvector of the linear transformation $f$ with eigenvalue $μ$ if and only if $f(x) = μx$.
More concisely: For any commutative ring `R`, additive commutative group `M`, and `R`-module `M`, a linear transformation `f` from `M` to `M`, scalar `μ` in `R`, and vector `x` in `M`, `x` is an eigenvector of `f` with eigenvalue `μ` if and only if `f(x) = μ × x`.
|
Module.End.hasGeneralizedEigenvalue_iff_hasEigenvalue
theorem Module.End.hasGeneralizedEigenvalue_iff_hasEigenvalue :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
{μ : R} {k : ℕ}, 0 < k → (f.HasGeneralizedEigenvalue μ k ↔ f.HasEigenvalue μ)
This theorem states that for any commutative ring `R`, any additively commutative group `M`, any module `M` over the ring `R`, any linear endomorphism `f` of the module `M`, any element 'μ' of the ring `R`, and any natural number `k` such that `k` is greater than 0, having a generalized eigenvalue is equivalent to having an eigenvalue. In other words, if `f` has a generalized eigenvalue 'μ' of order 'k', then `f` also has 'μ' as an eigenvalue, and vice versa.
More concisely: For any commutative ring `R`, additively commutative group `M`, module `M` over `R`, linear endomorphism `f` of `M`, element `μ` of `R`, and natural number `k` greater than 0, if `f` has a generalized eigenvalue `μ` of order `k`, then `μ` is an eigenvalue of `f`.
|
Module.End.eigenspace_restrict_le_eigenspace
theorem Module.End.eigenspace_restrict_le_eigenspace :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
{p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) (μ : R),
Submodule.map p.subtype (Module.End.eigenspace (LinearMap.restrict f hfp) μ) ≤ f.eigenspace μ
The theorem states that for a given endomorphism `f` of a module `M` over a commutative ring `R` and an invariant submodule `p` of `M` under `f`, the `μ`-eigenspace of the restriction of `f` to `p` is a submodule of the `μ`-eigenspace of `f`. In other words, if `p` is a submodule such that for all `x` in `p`, `f(x)` is also in `p`, then the set of vectors in `p` that are scaled by a factor of `μ` under the restricted operation of `f` is a subset of the set of all vectors in `M` that are scaled by `μ` under the operation of `f`.
More concisely: If `p` is an `F-`invariant submodule of an `R-`module `M` with respect to an endomorphism `F`, then the `μ-`eigenspace of `F|p` (restriction of `F` to `p`) is contained in the `μ-`eigenspace of `F` on `M`.
|
Module.End.hasEigenvalue_of_hasGeneralizedEigenvalue
theorem Module.End.hasEigenvalue_of_hasGeneralizedEigenvalue :
∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
{μ : R} {k : ℕ}, f.HasGeneralizedEigenvalue μ k → f.HasEigenvalue μ
The theorem `Module.End.hasEigenvalue_of_hasGeneralizedEigenvalue` states that for any commutative ring `R`, any additive commutative group `M`, and any `R`-module structure on `M`, given any linear endomorphism `f` of `M`, any element `μ` of `R`, and any natural number `k`, if `f` has a generalized eigenvalue `μ` of order `k`, then `f` also has an eigenvalue `μ`. This is to say, every generalized eigenvalue of a linear endomorphism is also an eigenvalue.
More concisely: If an endomorphism of an R-module has a generalized eigenvalue of order k with eigenvalue μ (over a commutative ring R), then it has an eigenvalue equal to μ.
|