From 029b2587d7ef6afee2fbcd616279dbb9a587899d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 11 Dec 2020 16:44:06 +0000
Subject: [PATCH] chore(linear_algebra/tensor_product): Actually relax the
 requirements for add_comm_group (#5315)

A previous commit (#5305) changed the definition to not need these, but forgot to actually change these.
---
 src/linear_algebra/tensor_product.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/linear_algebra/tensor_product.lean b/src/linear_algebra/tensor_product.lean
index 1b2251f509b9e..c85418bb450f8 100644
--- a/src/linear_algebra/tensor_product.lean
+++ b/src/linear_algebra/tensor_product.lean
@@ -710,12 +710,12 @@ end semiring
 
 section ring
 
-variables {R : Type*} [comm_ring R]
+variables {R : Type*} [comm_semiring R]
 variables {M : Type*} {N : Type*} {P : Type*} {Q : Type*} {S : Type*}
 
 variables [add_comm_group M] [add_comm_group N] [add_comm_group P] [add_comm_group Q]
   [add_comm_group S]
-variables [module R M] [module R N] [module R P] [module R Q] [module R S]
+variables [semimodule R M] [semimodule R N] [semimodule R P] [semimodule R Q] [semimodule R S]
 
 namespace tensor_product