English
The Hermitian-ness of fromBlocks A B C D is equivalent to A being Hermitian, Bᴴ = C, Cᴴ = B, and D Hermitian.
Русский
Эрмитовость fromBlocks A B C D эквивалентна тому, что A эрмитова, Bᴴ = C, Cᴴ = B и D эрмитова.
LaTeX
$$$ (A.fromBlocks B C D).IsHermitian \iff A.IsHermitian ∧ B^{\mathsf{H}} = C ∧ C^{\mathsf{H}} = B ∧ D.IsHermitian $$$
Lean4
/-- This is the `iff` version of `Matrix.IsHermitian.fromBlocks`. -/
theorem isHermitian_fromBlocks_iff {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} :
(A.fromBlocks B C D).IsHermitian ↔ A.IsHermitian ∧ Bᴴ = C ∧ Cᴴ = B ∧ D.IsHermitian :=
⟨fun h => ⟨congr_arg toBlocks₁₁ h, congr_arg toBlocks₂₁ h, congr_arg toBlocks₁₂ h, congr_arg toBlocks₂₂ h⟩,
fun ⟨hA, hBC, _hCB, hD⟩ => IsHermitian.fromBlocks hA hBC hD⟩
