English
If ker(f^k) = ker(f^{k+1}) for a linear endomorphism f, then ker(f^k) = ker(f^{k+m}) for every m ≥ 0.
Русский
Если ядро(f^k) равно ядру(f^{k+1}) для линейного отображения f, то ядро(f^k) равно ядру(f^{k+m}) для любого m ≥ 0.
LaTeX
$$$\forall m, \operatorname{ker}(f^k) = \operatorname{ker}(f^{k+m})$ при условии $\operatorname{ker}(f^k) = \operatorname{ker}(f^{k+1})$$$
Lean4
theorem ker_pow_constant {f : End K V} {k : ℕ} (h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)) :
∀ m, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + m))
| 0 => by simp
| m + 1 => by
apply le_antisymm
· rw [add_comm, pow_add]
apply LinearMap.ker_le_ker_comp
·
rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m, Module.End.mul_eq_comp,
Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h, Nat.add_one]
