Theorems · Theorem · linear algebra

Module.End.generalized_eigenvec_disjoint_range_ker

∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (f : Module.End K V) (μ : K),
  Disjoint (f.genEigenrange μ ↑(Module.finrank K V)) ((f.genEigenspace μ) ↑(Module.finrank K V))

Generalized eigenrange and generalized eigenspace for exponent finrank K V are disjoint.

Defined in

Mathlib.LinearAlgebra.Eigenspace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleFiniteDimensional