# Zulip Chat Archive

## Stream: new members

### Topic: Tensor Products

#### Zhangir Azerbayev (Jul 05 2020 at 23:17):

Hi everyone. I'm trying to do some basic stuff with tensor products.

```
import tactic
import data.real.basic
import linear_algebra.basic
import linear_algebra.finite_dimensional
import linear_algebra.tensor_product
universe u
open tensor_product
variables (K V : Type u) [field K] [add_comm_group V] [module K V]
[finite_dimensional K V]
variables v w : V
#check V ⊗ₜ[K] V
#check v ⊗ₜ[K] w
```

The error message I'm getting is

```
failed to synthesize type class instance for
K V : Type u,
...
⊢ add_comm_group (Type u)
```

Does anyone know what `add_comm_group (Type u)`

means?

#### Mario Carneiro (Jul 05 2020 at 23:19):

It's trying to infer an instance of `add_comm_group`

for `Type`

, which doesn't have one because the universe is not a group

#### Mario Carneiro (Jul 05 2020 at 23:20):

This sometimes happens when you write things like `nat + int`

#### Mario Carneiro (Jul 05 2020 at 23:21):

The issue appears to be that `⊗ₜ`

is `tensor_group.tmul`

, which is the multiplication of *vectors* inside the tensor product. It is not the tensor product type itself

#### Mario Carneiro (Jul 05 2020 at 23:23):

The notation for the type itself is `V ⊗[K] V`

although it is in a locale that you have to open first

```
open_locale tensor_product
#check (v ⊗ₜ[K] w : V ⊗[K] V)
```

#### Zhangir Azerbayev (Jul 05 2020 at 23:28):

I see, thank you @Mario Carneiro . What is the difference between a namespace and a locale?

#### Mario Carneiro (Jul 05 2020 at 23:29):

`open_locale`

and `localized`

are mathlib notions (not part of lean core) for simulating namespaced notation

Last updated: May 08 2021 at 18:17 UTC