grunweg
Results
112
comments of
grunweg
The privateModule linter *not* firing is hopefully fixed by #32140: let's wait for that PR to verify the fix here.
Can you also update `1000.yaml` once you finish proving the theorem? Completing a named theorem should be celebrated appropriately :-)