Zulip Chat Archive
Stream: general
Topic: quadratic reciprocity
Kenny Lau (Oct 10 2018 at 20:19):
@Mario Carneiro do you feel like quadratic_reciprocity.lean has too many long theorems?
Chris Hughes (Oct 10 2018 at 20:33):
I wasn't too happy with that aspect of the proof, but it is quite difficult to avoid.
Last updated: Dec 20 2023 at 11:08 UTC