∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (A : Matrix m m α) (B : Matrix m n α) {D : Matrix n n α},
  D.IsHermitian → ((Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (A - B * D⁻¹ * B.conjTranspose).IsHermitian)