Priority of tensor_product notation.

Stream: general

[Antoine Labelle]

I get an error in the following code because lean thinks that ⊗ means representation.tprod while I want to use the tensor product coming from the monoidal category fdRep. How can I get lean to use the right tensor product?

import representation_theory.fdRep
import representation_theory.basic

universes u

namespace fdRep

variables {k G : Type u} [field k]
variables [monoid G] (V W : fdRep k G)

def character (g : G) := linear_map.trace k V (V.ρ g)

lemma char_tensor : (V ⊗ W).character = V.character * W.character := sorry

end fdRep

[Floris van Doorn]

We should change the global notation for representation.tprod into a localized one in mathlib. I think we should not have ⊗ as global notation.

[Floris van Doorn]

For the moment, you can use local infix ` ⊗ ` := fdRep (untested)

[Floris van Doorn]

I mean local infixr ` ⊗ ` := category_theory.monoidal_category.tensor_obj.