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
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