Def Lean.Name.requiredModules

Modification history

2024-01-10 11:53
Mathlib/Lean/Expr/Basic.lean
refactor: split `ImportGraph` into its own package. (#9169) …
Deleted Lean.Name.requiredModulesView on Github →
2023-07-17 07:05
Mathlib/Lean/Expr/Basic.lean
feat: #find_home (#5731)
Added Lean.Name.requiredModulesView on Github →