Zulip Chat Archive
Stream: PR reviews
Topic: !3#16586 `push_neg` option
Violeta Hernández (Oct 22 2024 at 11:06):
I think you've got the number wrong, #16586 is one of my own PRs! sorry I forgot about mathlib3
Last updated: May 02 2025 at 03:31 UTC