(Coalgebra/TensorProduct): docstring.

Author: kbuzzard

FLT/for_mathlib/Coalgebra/TensorProduct.lean

@@ -9,10 +9,13 @@ import Mathlib.RingTheory.Bialgebra
 import FLT.for_mathlib.Coalgebra.Sweedler
 
 /-!
+
 # Tensor Product of Coalgebras
 
-Suppose `A, B` are `R`-coalgebras, then `A ⊗ B` has a natural `R`-coalgebra strucutre
-induced by those of `A` and `B`.
+Suppose `A, B` are `R`-coalgebras. Then `A ⊗[R] B` has a natural `R`-coalgebra structure.
+
+If furthermore `A` and `B` are `R`-bialgebras, then `A ⊗[R] B` has a natural
+`R`-bialgebra structure.
 
 -/