Finset.Prod: ambigiuous notation

Stream: mathlib4

[Arien Malec]

I had a look at this file, but got tired of inserting explicit annotations -- seems like there's something broken with precedence of ×ˢ

[Yaël Dillies]

Oh that's really sad. I overloaded the notation because in Lean 3 it "just works".

[Eric Wieser]

Based on Mario's comment elsewhere about tensor product notation I would expect this to be fairly easy to solve

[Heather Macbeth]

In that case, let's pause the file until we figure it out -- don't want to lose the notation if there is a way to keep it.

[Johan Commelin]

It's already merged. We have

--Porting note: Change notation from  "×ˢ" to "×ᶠ" to avoid ambiguity
@[inherit_doc]
infixr:82
  " ×ᶠ " =>-- This notation binds more strongly than (pre)images, unions and intersections.
  Finset.product

for now.

[Johan Commelin]

I think we can try to make this notation work in parallel to continuing the port.