Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-30 08:29 08bb1125

View on Github →

chore(ring_theory/hahn_series): extract lemmas from slow definitions (#7737) This doesn't make them much faster, but it makes it easier to tell which bits are slow

Estimated changes