MinImports

📁 Source: Mathlib/Tactic/Linter/MinImports.lean

Statistics

Metric	Count
Definitions «command#import_bumps», minImports, increases, «command#reset_min_imports»	4
Theorems	0
Total	4

Mathlib.Linter

Definitions

Name	Category	Theorems
«command#reset_min_imports» 📖	CompOp	—

Mathlib.Linter.MinImports

Definitions

Name	Category	Theorems
«command#import_bumps» 📖	CompOp	—

Mathlib.Linter.linter

Definitions

Name	Category	Theorems
minImports 📖	CompOp	—

Mathlib.Linter.linter.minImports

Definitions

Name	Category	Theorems
increases 📖	CompOp	—

---

← Back to Index