English
If m ≥ finrank_K V, then ker(f^m) = ker(f^{finrank_K V}) for f ∈ End_K(V).
Русский
Если m ≥ dim_K V, то ker(f^m) = ker(f^{dim_K V}) для эндоморфизма f.
LaTeX
$$$\\operatorname{ker}(f^m) = \\operatorname{ker}(f^{\\operatorname{finrank}_K V})$ when $m \\ge \\operatorname{finrank}_K V$.$$
Lean4
theorem exists_ker_pow_eq_ker_pow_succ [FiniteDimensional K V] (f : End K V) :
∃ k : ℕ, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ) := by
classical
by_contra h_contra
simp_rw [not_exists, not_and] at h_contra
have h_le_ker_pow : ∀ n : ℕ, n ≤ (finrank K V).succ → n ≤ finrank K (LinearMap.ker (f ^ n)) :=
by
intro n hn
induction n with
| zero => exact zero_le (finrank _ _)
| succ n
ih =>
have h_ker_lt_ker : LinearMap.ker (f ^ n) < LinearMap.ker (f ^ n.succ) :=
by
refine lt_of_le_of_ne ?_ (h_contra n (Nat.le_of_succ_le_succ hn))
rw [pow_succ']
apply LinearMap.ker_le_ker_comp
have h_finrank_lt_finrank : finrank K (LinearMap.ker (f ^ n)) < finrank K (LinearMap.ker (f ^ n.succ)) := by
apply Submodule.finrank_lt_finrank_of_lt h_ker_lt_ker
calc
n.succ ≤ (finrank K ↑(LinearMap.ker (f ^ n))).succ := Nat.succ_le_succ (ih (Nat.le_of_succ_le hn))
_ ≤ finrank K ↑(LinearMap.ker (f ^ n.succ)) := Nat.succ_le_of_lt h_finrank_lt_finrank
have h_any_n_lt : ∀ n, n ≤ (finrank K V).succ → n ≤ finrank K V := fun n hn =>
(h_le_ker_pow n hn).trans (Submodule.finrank_le _)
exact Nat.not_succ_le_self _ (h_any_n_lt (finrank K V).succ (finrank K V).succ.le_refl)
