pow_row_eq_zero_of_le — Mathlib

English

If a row of a power of a matrix is zero at power k, then for any l ≥ k the row is still zero: (M^k).row i = 0 and k ≤ l implies (M^l).row i = 0.

Русский

Если строка i матрицы M становится нулевой на степени k, то при любой степени l ≥ k она остаётся нулевой.

LaTeX

$$$\\bigl((M^k)\\bigr).row_i = 0 \\Rightarrow k \\le l \\Rightarrow (M^l).row_i = 0$$$

Lean4

theorem pow_row_eq_zero_of_le [Fintype n] [DecidableEq n] {M : Matrix n n R} {k l : ℕ} {i : n} (h : (M ^ k).row i = 0)
    (h' : k ≤ l) : (M ^ l).row i = 0 :=
  by
  replace h' : l = k + (l - k) := by omega
  rw [← single_one_vecMul] at h ⊢
  rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]

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