Def redundantImports

Modification history

2024-01-10 11:53

Mathlib/Util/Imports.lean

refactor: split `ImportGraph` into its own package. (#9169) …

Deleted redundantImports View on Github →

2023-06-28 11:45

Mathlib/Util/Imports.lean

feat: #redundant_imports / #minimize_imports commands (#5441) …

Added redundantImports View on Github →