Theorems · Theorem · linear algebra

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.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k))
      ⋯),
  IsNilpotent (LinearMap.restrict (f - (algebraMap R (Module.End R M)) μ) h)

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

Defined in

Mathlib.LinearAlgebra.Eigenspace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule