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)