Commit 2024-11-11 15:53 d15f04e1

View on Github →

fix: silence the linter in files not imported by Mathlib.lean (#18033) Zulip

Estimated changes