eRank_diagonal — Mathlib

English

For the diagonal matrix diag(w), its eRank equals the encard of the set of indices where w is nonzero.

Русский

Для диагональной матрицы diag(w) её eRank равен encard множества индексов i, удовлетворяющих w(i) ≠ 0.

LaTeX

$$$ (\mathrm{diag}(w)).\mathrm{eRank} = \operatorname{encard} \{ i \mid w(i) \neq 0 \}. $$$

Lean4

theorem eRank_diagonal [DecidableEq m] (w : m → R) : (diagonal w).eRank = {i | (w i) ≠ 0}.encard := by
  simp [eRank, cRank_diagonal, toENat_cardinalMk_subtype]

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