rank_diagonal — Mathlib

English

The rank of a diagonal matrix equals the number of nonzero diagonal entries.

Русский

Ранг диагональной матрицы равен числу ненулевых диагональных элементов.

LaTeX

$$$\operatorname{rank}(\operatorname{diagonal}(w)) = \#\{i : w(i) \neq 0\}$$$

Lean4

/-- The rank of a diagonal matrix is the count of non-zero elements on its main diagonal -/
theorem rank_diagonal [Fintype m] [DecidableEq m] [DecidableEq R] (w : m → R) :
    (diagonal w).rank = Fintype.card { i // (w i) ≠ 0 } := by
  rw [Matrix.rank, ← Matrix.toLin'_apply', Module.finrank, ← LinearMap.rank, LinearMap.rank_diagonal,
    Cardinal.toNat_natCast]

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