∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] [inst_3 : StarAddMonoid α] [NormedStarGroup α] (A : Matrix m n α),
  ‖A.conjTranspose‖ = ‖A‖