Theorems · Theorem · linear algebra

Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo

∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  (f g : Module.End R M) (hf : Set.MapsTo ⇑f ↑p ↑p) (hg : Set.MapsTo ⇑g ↑p ↑p) {μ₁ μ₂ : R},
  Set.MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂) →
    Set.MapsTo ⇑(LinearMap.restrict f hf) ↑(Module.End.maxGenEigenspace (LinearMap.restrict g hg) μ₁)
      ↑(Module.End.maxGenEigenspace (LinearMap.restrict g hg) μ₂)

Defined in

Mathlib.LinearAlgebra.Eigenspace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule