ker_pow_le_ker_pow_finrank — Mathlib

English

In a finite-dimensional K-vector space V with f ∈ End_K(V), ker(f^m) ≤ ker(f^{finrank K V}) for all m.

Русский

В конечномерном пространстве V над K и эндоморфизме 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_le_ker_pow_finrank [FiniteDimensional K V] (f : End K V) (m : ℕ) :
    LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V) :=
  by
  by_cases h_cases : m < finrank K V
  · rw [← add_tsub_cancel_of_le (Nat.le_of_lt h_cases), add_comm, pow_add]
    apply LinearMap.ker_le_ker_comp
  · rw [ker_pow_eq_ker_pow_finrank_of_le (le_of_not_gt h_cases)]

Похожие утверждения