binary product notation has wrong precedence

Stream: mathlib4

[Kenny Lau]

import Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

instance : CategoryTheory.Limits.HasBinaryProduct ℕ ℕ := sorry

#check ℕ = ℕ ⨯ ℕ   -- @CategoryTheory.Limits.prod Prop ?m.147 (ℕ = ℕ) ℕ
#check ℕ = (ℕ ⨯ ℕ) -- works

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/8b8fe2fa631658e55895b284747a997a249d3599/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean#L503

/-- Notation for the product -/
notation:20 X " ⨯ " Y:20 => prod X Y

[Kenny Lau]

i think this bug is happening because 20 is too low? or maybe this is intended?

[Johan Commelin]

Hmmz, I doubt this is intended. Please PR a fix :smiley:

[Kenny Lau]

what is the correct number?

[Johan Commelin]

Je ne sais pas :shrug:

[Aaron Liu]

I seem to remember that equality is 50, so you should make it more than that

[Kevin Buzzard]

* is 70 (and Prod is 30)