Mathlib Changelog
v4
Changelog
About
Github
Def
Mathlib.Linter.DirectoryDependency.NamePrefixRel
Modification history
2025-03-31 05:22
Mathlib/Tactic/Linter/DirectoryDependency.lean
feat(Tactic/Linter): a linter for directory dependencies (#23088) …
Added
Mathlib.Linter.DirectoryDependency.NamePrefixRel
View on Github →