tensor product

Stream: new members

[Sam Lichtenstein]

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]

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]

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

[Sam Lichtenstein]

thanks!