∀ (m : Type u_1) (n : Type u_2) (α : Type u_3) [inst : AddCommMonoid α] [inst_1 : StarAddMonoid α] (x y : Matrix m n α),
  (Matrix.conjTransposeAddEquiv m n α).toFun (x + y) =
    (Matrix.conjTransposeAddEquiv m n α).toFun x + (Matrix.conjTransposeAddEquiv m n α).toFun y