Zulip Chat Archive
Stream: PR reviews
Topic: mathlib4#896
Scott Morrison (Dec 07 2022 at 22:58):
Should be straightforward, already approved by @Ruben Van de Velde.
Last updated: Dec 20 2023 at 11:08 UTC
Should be straightforward, already approved by @Ruben Van de Velde.
Last updated: Dec 20 2023 at 11:08 UTC