Zulip Chat Archive

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):


Last updated: Dec 20 2023 at 11:08 UTC