English
For a finite-dimensional K-vector space V and f ∈ End_K(V), ker(f^m) ≤ ker(f^{finrank_K V}) for any m.
Русский
Для конечномерного пространства V и эндоморфизма f верно: ker(f^m) ≤ ker(f^{finrank_K V}) для любого m.
LaTeX
$$$\\ker(f^m) \\le \\ker(f^{\\operatorname{finrank}_K V})$.$$
Lean4
theorem ker_pow_eq_ker_pow_finrank_of_le [FiniteDimensional K V] {f : End K V} {m : ℕ} (hm : finrank K V ≤ m) :
LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V) :=
by
obtain ⟨k, h_k_le, hk⟩ : ∃ k, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ) :=
exists_ker_pow_eq_ker_pow_succ f
calc
LinearMap.ker (f ^ m) = LinearMap.ker (f ^ (k + (m - k))) := by rw [add_tsub_cancel_of_le (h_k_le.trans hm)]
_ = LinearMap.ker (f ^ k) := by rw [ker_pow_constant hk _]
_ = LinearMap.ker (f ^ (k + (finrank K V - k))) := (ker_pow_constant hk (finrank K V - k))
_ = LinearMap.ker (f ^ finrank K V) := by rw [add_tsub_cancel_of_le h_k_le]
