English
If the block matrix fromBlocks 0 C D is symmetric and A and D are diagonal, then the full fromBlocks is diagonal.
Русский
Если блочная матрица fromBlocks 0 C D симметрична, а A и D диагональны, то вся матрица fromBlocks диагональная.
LaTeX
$$$\\forall {\\alpha} {A : Matrix m m \\alpha} {C : Matrix n m \\alpha} {D : Matrix n n \\alpha}
(h : (A.fromBlocks 0 C D).IsSymm) (ha : A.IsDiag) (hd : D.IsDiag) : (A.fromBlocks 0 C D).IsDiag$$$
Lean4
/-- The block matrix `A.fromBlocks 0 0 D` is diagonal if `A` and `D` are diagonal. -/
theorem fromBlocks [Zero α] {A : Matrix m m α} {D : Matrix n n α} (ha : A.IsDiag) (hd : D.IsDiag) :
(A.fromBlocks 0 0 D).IsDiag := by
rintro (i | i) (j | j) hij
· exact ha (ne_of_apply_ne _ hij)
· rfl
· rfl
· exact hd (ne_of_apply_ne _ hij)
