feat(*): localized `R[X]` notation for `polynomial R` (#11895)
I did not change `polynomial (complex_term_here taking args)` in many places because I thought it would be more confusing. Also, in some files that prove things about polynomials incidentally, I also did not include the notation and change the files.
Co-authored-by: Johan Commelin <johan@commelin.net>
