Aggressive notation, Y

Stream: mathlib4

[Eric Wieser]

In the following code, the letter Y ends up as a syntax error

import Mathlib -- works fine with a smaller import

open Polynomial

theorem something_polynomial : X + 1 ≠ (0 : ℚ[X]) := sorry  -- ok
theorem something_not_polynomial (X : Nat) : X + 1 ≠ 0 := sorry  -- ok

theorem something_polynomial2 : Y + 1 ≠ (0 : ℚ[X][Y]) := sorry  -- ok
theorem something_not_polynomial2 (Y : Nat) : X + 1 ≠ 0 := sorry  -- syntax error

Should we replace docs#Polynomial.termY with an abbrev instead?

[Eric Wieser]

cc @Junyan Xu

[Eric Wieser]

Another option would be to move it into the Polynomial.Bivariate scope instead of Polynomial

[Junyan Xu]

Or PolynomialPolynomial scope as was originally the case; see the poll here.

[Eric Wieser]

#19292 moves it to Polynomial.Bivariate; feel free to push a different namespace to that PR, or switch it to abbrev.