Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-11-19 11:57
52318983
View on Github →
chore(Linter/TextBased): remove dead code (
#31800
)
Estimated changes
Modified
Mathlib/Tactic/Linter/TextBased.lean
deleted
inductive
Mathlib.Linter.TextBased.BroadImports