Theorems · Definition · linear algebra

Module.End.HasUnifEigenvector

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

Let M be an R-module, and f an R-linear endomorphism of M, and let μ : R and k : ℕ∞ be given. Then x : M satisfies HasUnifEigenvector f μ k x if x ∈ f.genEigenspace μ k and x ≠ 0. For k = 1, this means that x is an eigenvector of f with eigenvalue μ.

Defined in

Mathlib.LinearAlgebra.Eigenspace.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule