{m : Type u_1} →
  {n : Type u_2} →
    (R : Type u_3) →
      (A : Type u_5) →
        {l : Type u_7} →
          {o : Type u_8} →
            [inst : Semiring R] →
              [inst_1 : AddCommMonoid A] →
                [inst_2 : Module R A] → m ≃ l → n ≃ o → CStarMatrix m n A ≃ₗ[R] CStarMatrix l o A