Theorems · Definition · linear algebra

Module.End.HasUnifEigenvalue

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

Let M be an R-module, and f an R-linear endomorphism of M. Then μ : R and k : ℕ∞ satisfy HasUnifEigenvalue f μ k if f.genEigenspace μ k ≠ ⊥. For k = 1, this means that μ is an eigenvalue of f.

Defined in

Mathlib.LinearAlgebra.Eigenspace.Basic

Cited by

18 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule