English
The block-matrix fromBlocks construction is symmetric if and only if A is symmetric, B^T = C, D is symmetric.
Русский
Блочная матрица из блоков A.fromBlocks B C D симметрична тогда и только тогда, когда A симметрична, B^T = C, и D симметрична.
LaTeX
$$$(A.fromBlocks B C D)^{T}=A.fromBlocks B C D\iff A^{T}=A \land B^{T}=C \land C^{T}=B \land D^{T}=D$$$
Lean4
/-- This is the `iff` version of `Matrix.isSymm.fromBlocks`. -/
theorem isSymm_fromBlocks_iff {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} :
(A.fromBlocks B C D).IsSymm ↔ A.IsSymm ∧ Bᵀ = C ∧ Cᵀ = B ∧ D.IsSymm :=
⟨fun h =>
⟨(congr_arg toBlocks₁₁ h :), (congr_arg toBlocks₂₁ h :), (congr_arg toBlocks₁₂ h :), (congr_arg toBlocks₂₂ h :)⟩,
fun ⟨hA, hBC, _, hD⟩ => IsSymm.fromBlocks hA hBC hD⟩
