Def Mathlib.Linter.DirectoryDependency.NamePrefixRel

Modification history

2025-12-05 11:03
Mathlib/Tactic/Linter/DirectoryDependency.lean
chore(Tactic/Linters): remove `public section` (#31803) …
Modified Mathlib.Linter.DirectoryDependency.NamePrefixRelView on Github →
2025-11-19 06:07
Mathlib/Tactic/Linter/DirectoryDependency.lean
chore: move Mathlib to the module system (#31786) …
Modified Mathlib.Linter.DirectoryDependency.NamePrefixRelView on Github →
2025-03-31 05:22
Mathlib/Tactic/Linter/DirectoryDependency.lean
feat(Tactic/Linter): a linter for directory dependencies (#23088) …
Added Mathlib.Linter.DirectoryDependency.NamePrefixRelView on Github →