submatrix — Mathlib

English

If A is diagonal, then any diagonal submatrix formed via an injective index map f is also diagonal.

Русский

Если A диагональная, то любая диагональная подматрица, полученная с помощью инъективного отображения индексов, тоже диагональная.

LaTeX

$$$\\forall {\\alpha} [Zero \\alpha] {A : Matrix n n \\alpha} (ha : A.IsDiag) {f : m \\to n} (hf : Injective f) : (A.submatrix f f).IsDiag$$$

Lean4

theorem submatrix [Zero α] {A : Matrix n n α} (ha : A.IsDiag) {f : m → n} (hf : Injective f) :
    (A.submatrix f f).IsDiag := fun _ _ h => ha (hf.ne h)

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