Theorems · Definition · linear algebra

Module.End.genEigenspace

{R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ∞ →o Submodule R M

The submodule genEigenspace f μ k for a linear map f, a scalar μ, and a number k : ℕ∞ is the kernel of (f - μ • id) ^ k if k is a natural number, or the union of all these kernels if k = ∞. (k = ∞ corresponds to Def 8.19 of [axler2024].) A generalized eigenspace for some exponent k is contained in the generalized eigenspace for exponents larger than k.

Defined in

Mathlib.LinearAlgebra.Eigenspace.Basic

Cited by

70 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule