∀ {R : Type u_6} [inst : CommSemiring R] {A : Type u_7} [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (n : ℤ),
  CoalgebraStruct.comul (LaurentPolynomial.T n) = LaurentPolynomial.T n ⊗ₜ[R] LaurentPolynomial.T n