Zulip Chat Archive
Stream: condensed mathematics
Topic: commsq
Johan Commelin (Jul 27 2022 at 10:43):
We should refactor LTE's commsq into mathlib's comm_sq. Anyone want to work on that PR?
Scott Morrison (Jul 27 2022 at 10:43):
Sorry if I made negative progress by duplicating... :-(
Johan Commelin (Jul 27 2022 at 10:45):
No worries. The mathlib version is cleaner!
Johan Commelin (Jul 27 2022 at 10:45):
And 95% of the refactor should be a global-search-replace.
Last updated: Dec 20 2023 at 11:08 UTC