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]