mathlib

62c0a4ef - chore(*): consistently use R[X] notation for polynomials (#17044)

chore(*): consistently use R[X] notation for polynomials (#17044) Consistently use `R[X]` in favour of `polynomial R`. The exceptions that I've left as is are the cases where `R` itself includes an identifier or more brackets. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>