case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : ¬m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
by_cases h_cases : m < finrank K V
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ (finrank K V - m) * f ^ m)
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
rw [← add_tsub_cancel_of_le (Nat.le_of_lt h_cases), add_comm, pow_add]
no goals
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ (finrank K V - m) * f ^ m)
apply LinearMap.ker_le_ker_comp
no goals
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : ¬m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
rw [ker_pow_eq_ker_pow_finrank_of_le (le_of_not_lt h_cases)]