Zulip Chat Archive
Stream: PR reviews
Topic: mathlib4#572
Moritz Doll (Nov 13 2022 at 23:50):
@Scott Morrison since you are on a merging spree, could you merge this, too? I was about to correct some of these things again..
Last updated: Dec 20 2023 at 11:08 UTC