Mathlib Changelog
v4
Changelog
About
Github
Def
Mathlib.Linter.DirectoryDependency.NamePrefixRel.getAllLeft
Modification history
2025-05-28 07:47
Mathlib/Tactic/Linter/DirectoryDependency.lean
feat(Tactic/Linter/DirectoryDependency): add an allow-list for directories with few imports (#24109) …
Added
Mathlib.Linter.DirectoryDependency.NamePrefixRel.getAllLeft
View on Github →