α : Type u_1
β : Type ?u.26056
R : Type ?u.26059
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : IsSymm (Matrix.fromBlocks A 0 C D)
ha : IsDiag A
hd : IsDiag D
⊢ IsDiag (Matrix.fromBlocks A 0 0ᵀ D)
α : Type u_1
β : Type ?u.26056
R : Type ?u.26059
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : IsSymm (Matrix.fromBlocks A 0 C D)
ha : IsDiag A
hd : IsDiag D
⊢ IsDiag (Matrix.fromBlocks A 0 C D)
rw [← (isSymm_fromBlocks_iff.1 h).2.1]
no goals
α : Type u_1
β : Type ?u.26056
R : Type ?u.26059
n : Type u_3
m : Type u_2
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : IsSymm (Matrix.fromBlocks A 0 C D)
ha : IsDiag A
hd : IsDiag D
⊢ IsDiag (Matrix.fromBlocks A 0 0ᵀ D)
exact ha.fromBlocks hd