Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-29 14:36
fc4e2273
View on Github →
fix: silence
linter.minImports
tests (
#18372
) Reported on
Zulip
Estimated changes
Modified
Mathlib/Tactic/Linter/MinImports.lean
Modified
test/MinImports.lean