Zulip Chat Archive
Stream: mathlib4
Topic: Status of `Algebra.Group.Commute`?
Arien Malec (Nov 20 2022 at 21:29):
It has almost but not entirely all the content ported....
Scott Morrison (Nov 20 2022 at 21:30):
I think it is just an ad-hoc port. I don't see any PR that mentions it.
Last updated: May 02 2025 at 03:31 UTC