tensor product notation issue

Stream: general

[Kevin Buzzard]

I was writing down a definition of Picard groups in Lean and I ran into the below notation issue. How am I supposed to be working here?

import linear_algebra.tensor_product
import ring_theory.noetherian
import algebra.category.Module.abelian
import algebra.category.Module.monoidal

--open_locale tensor_product -- comment this line out fixes something
-- and breaks something else

variables (R M N : Type) [comm_ring R] [add_comm_group M] [module R M]
[add_comm_group N] [module R N]

-- works iff locale open
theorem fg_of_pseudoinvertible :
  nonempty (linear_equiv R (M ⊗[R] N) R) → submodule.fg (⊤ : submodule R M) :=
sorry

-- works iff locale not open
def pseudoinvertible (A : Module R) : Prop :=
∃ B, nonempty (A ⊗ B ≅ 𝟙_ (Module R))

[Alex J. Best]

In sections? Looks like the notations for tensor product of unbundled modules clashes with that for bundled modules (as a monoidal category) right so just stick to one within a section.
Alternatively opening the locale and then doing

infixr ` ⊗ `:70 := category_theory.monoidal_category.tensor_obj
infixr ` ⊗ `:70 := category_theory.monoidal_category.tensor_hom

works

[Eric Wieser]

Are those the same symbol or different symbols?