English
A symmetric block matrix fromBlocks A 0 C D is diagonal if A and D are diagonal and B is zero; this is a restatement in a symmetric context.
Русский
Симметричная блочная матрица fromBlocks диагональна, если A и D диагональны, а B = 0.
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
/-- A symmetric block matrix `A.fromBlocks B C D` is diagonal
if `A` and `D` are diagonal and `B` is `0`. -/
theorem fromBlocks_of_isSymm [Zero α] {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α}
(h : (A.fromBlocks 0 C D).IsSymm) (ha : A.IsDiag) (hd : D.IsDiag) : (A.fromBlocks 0 C D).IsDiag :=
by
rw [← (isSymm_fromBlocks_iff.1 h).2.1]
exact ha.fromBlocks hd
