## Stream: new members

### Topic: tensor product

#### Sam Lichtenstein (Jun 04 2020 at 02:28):

How do I use infix notation for tensor products?

import linear_algebra.tensor_product

universes u v w
variables (R : Type u)
variables [comm_ring R]
variables (M N : Type u)
variables [add_comm_group M] [add_comm_group N] [module R M] [module R N]

#check tensor_product R M N -- seems to work fine
open tensor_product -- this doesn't seem to make a difference, with or without it I get:
#check M ⊗[R] N -- error : unexpected token


#### Mario Carneiro (Jun 04 2020 at 02:39):

The notation is declared like so:

localized "infix  ⊗ :100 := tensor_product _" in tensor_product
localized "notation M  ⊗[:100 R ]  N:100 := tensor_product R M N" in tensor_product


This means it is a localized notation, which means it is local to a file but can be reopened using open_locale tensor_product

#### Mario Carneiro (Jun 04 2020 at 02:40):

(These "locales" are separate from lean's "namespaces" and so open doesn't work; they are enabled by some tactics in mathlib.)

#### Sam Lichtenstein (Jun 04 2020 at 02:42):

thanks!

Last updated: May 14 2021 at 06:16 UTC