∀ {ι : Type u_1} {R : Type u_2} {A : ι → Type u_3} [inst : CommRing R] [inst_1 : (i : ι) → CommRing (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] (a b : PiTensorProduct R fun i => A i), a - b = a + -b