Closed digama0 closed 1 year ago
bors merge
Oops, no bors here, I guess.
oh, the commit SHA has to be changed here after the corresponding mathlib4 PR gets merged since the bors commit has a different SHA
bors merge