∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Star R] (A₁ : Matrix m n₁ R)
  (A₂ : Matrix m n₂ R), (A₁.fromCols A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose