Theorems · Theorem · linear algebra

Module.End.isNilpotent_restrict_genEigenspace_nat

∀ {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 - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)) ⋯),
  IsNilpotent (LinearMap.restrict (f - μ • 1) h)

The restriction of f - μ • 1 to the k-fold generalized μ-eigenspace is nilpotent.

Defined in

Mathlib.LinearAlgebra.Eigenspace.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule