Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-08 15:58 201a3f4a

View on Github →

chore(*): remove extra parentheses in universe annotations (#14595) We change f.{(max u v)} to f.{max u v} throughout, and similarly for imax. This is for consistency with the rest of the code. Note that max and imax take an arbitrary number of parameters, so if anyone wants to add a second universe parameter, they'll have to add the parentheses again.

Estimated changes