Closed eric-wieser closed 2 years ago
The repository this links to no longer exists
This was already applied to mathlib as https://github.com/leanprover-community/mathlib/pull/13906
The repository this links to no longer exists
This was already applied to mathlib as https://github.com/leanprover-community/mathlib/pull/13906