Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-08 19:36 4ee67acb

View on Github →

chore(*): use prod notation (#2989) The biggest field test of the new product notation.

Estimated changes