Zulip Chat Archive
Stream: mathlib4
Topic: !4#3192
Jeremy Tan (Mar 30 2023 at 10:46):
!4#3192 I'd like help in solving the 5 remaining errors in this file
Moritz Firsching (Mar 31 2023 at 09:53):
I fixed the remaining 5 errors
Jeremy Tan (Mar 31 2023 at 13:59):
right
Last updated: Dec 20 2023 at 11:08 UTC