Zulip Chat Archive
Stream: Copenhagen Masterclass 2023
Topic: Ab is AB5
David Ang (Jun 30 2023 at 15:18):
This is pretty much done, and we’re committing straight to mathlib4.
David Ang (Jun 30 2023 at 15:19):
@Moritz Firsching @Nikolas Kuhn there is an error in my local file that I need to fix
Moritz Firsching (Jun 30 2023 at 15:36):
Ok
David Ang (Jul 10 2023 at 01:16):
This is also done: #5597
Last updated: Dec 20 2023 at 11:08 UTC