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 2025 at 21:32 UTC
Should be straightforward, already approved by @Ruben Van de Velde.
Last updated: Dec 20 2025 at 21:32 UTC