Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-29 22:56 62c0a4ef

View on Github →

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.

Estimated changes