Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-12 17:53 a7d872fa

View on Github →

chore(category/abelian/pseudoelements): localize expensive typeclass (#9156) Per @fpvandoorn's new linter.

Estimated changes