Zulip Chat Archive
Stream: mathlib4
Topic: 1 error left in !4#5397 AddCharacter
Jeremy Tan (Jun 22 2023 at 21:12):
!4#5397 there's 1 error left here, can you fix it?
Jeremy Tan (Jun 23 2023 at 03:47):
Now it should be ready for review – onwards to quadratic reciprocity
Scott Morrison (Jun 23 2023 at 05:19):
A few minor bits of cleanup needed.
Jireh Loreaux (Jun 23 2023 at 14:54):
@Jeremy Tan that was a pretty short break from porting! :smiley:
Jeremy Tan (Jun 24 2023 at 05:55):
Jireh Loreaux said:
Jeremy Tan that was a pretty short break from porting! :smiley:
No, my break is more of a tailing-off of activity
Last updated: Dec 20 2023 at 11:08 UTC