Closed jcommelin closed 5 years ago
We can merge this after bumping mathlib. But at the moment PR 994 is not yet in the precompiled binaries.
We can merge this after bumping mathlib. But at the moment PR 994 is not yet in the precompiled binaries.