Def Mathlib.Linter.Style.header.duplicateImportsCheck

Modification history

2024-11-07 03:11
Mathlib/Tactic/Linter/Header.lean
feat: rewrite the duplicateImports linter (#17555) …
Added Mathlib.Linter.Style.header.duplicateImportsCheckView on Github →