Commit 2025-02-17 19:42 517a664b
View on Github →chore(NumberTheory/Harmonic): move some results downstream from Defs.lean (#21999)
This Defs file relies on quite a bit of theory. We can move the lemmas inside closer to the place of usage and shake imports that way. I don't know how important this is overall, but it does make for a nice local reduction.