K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map f (LinearMap.range ((f - ↑(algebraMap K (End K V)) μ) ^ n)) =
    LinearMap.range (f * (f - ↑(algebraMap K (End K V)) μ) ^ n)
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map f (generalizedEigenrange f μ n) = LinearMap.range (f * (f - ↑(algebraMap K (End K V)) μ) ^ n)
rw [generalizedEigenrange]
no goals
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ Submodule.map f (LinearMap.range ((f - ↑(algebraMap K (End K V)) μ) ^ n)) =
    LinearMap.range (f * (f - ↑(algebraMap K (End K V)) μ) ^ n)
exact (LinearMap.range_comp _ _).symm
no goals
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ LinearMap.range (f * (f - ↑(algebraMap K (End K V)) μ) ^ n) =
    LinearMap.range ((f - ↑(algebraMap K (End K V)) μ) ^ n * f)
rw [Algebra.mul_sub_algebraMap_pow_commutes]