Skip to content

Commit

Permalink
chore(linear_algebra/tensor_product): Actually relax the requirements…
Browse files Browse the repository at this point in the history
… for add_comm_group (#5315)

A previous commit (#5305) changed the definition to not need these, but forgot to actually change these.
  • Loading branch information
eric-wieser committed Dec 11, 2020
1 parent db712d5 commit 029b258
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/linear_algebra/tensor_product.lean
Expand Up @@ -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

Expand Down

0 comments on commit 029b258

Please sign in to comment.