Def Mathlib.Linter.DoubleImports.upstreamableDeclLinter

Modification history

2024-11-18 11:19
Mathlib/Tactic/Linter/UpstreamableDecl.lean
feat: the upstreamDecl linter (#18702) …
Added Mathlib.Linter.DoubleImports.upstreamableDeclLinterView on Github →