no goals
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + 0))
simp
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))

case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
m : ℕ
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + (m + 1)))
apply le_antisymm
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (m + 1) * f ^ k)
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))
rw [add_comm, pow_add]
no goals
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (m + 1) * f ^ k)
apply LinearMap.ker_le_ker_comp
no goals
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ Nat.succ k)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
  LinearMap.mul_eq_comp, LinearMap.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
  Nat.add_one]