pow_col_eq_zero_of_le — Mathlib

English

Analogous to rows: if (M^k).col i = 0 and k ≤ l, then (M^l).col i = 0.

Русский

Аналогично строкам: если (M^k).col i = 0 и k ≤ l, то (M^l).col i = 0.

LaTeX

$$$(M^k).col i = 0 \\land k \\le l \\Rightarrow (M^l).col i = 0$$$

Lean4

theorem pow_col_eq_zero_of_le [Fintype n] [DecidableEq n] {M : Matrix n n R} {k l : ℕ} {i : n} (h : (M ^ k).col i = 0)
    (h' : k ≤ l) : (M ^ l).col i = 0 :=
  by
  replace h' : l = (l - k) + k := by omega
  rw [← mulVec_single_one] at h ⊢
  rw [h', pow_add, ← mulVec_mulVec, h, mulVec_zero]

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