Zulip Chat Archive
Stream: mathlib4
Topic: Data.Int.Associated
Shreyas Srinivas (Dec 23 2022 at 23:27):
I am about to start the port of this file.
Shreyas Srinivas (Dec 23 2022 at 23:38):
PR: mathlib4#1195
Shreyas Srinivas (Dec 24 2022 at 00:03):
Ready for review
Last updated: Dec 20 2023 at 11:08 UTC