diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean
index 9f5be314fe2ff..19b353da35598 100644
--- a/Mathlib/Tactic/Linter/Header.lean
+++ b/Mathlib/Tactic/Linter/Header.lean
@@ -218,6 +218,15 @@ def isInMathlib (modName : Name) : IO Bool := do
     return (ml.map (·.module == modName)).any (·)
   else return false
 
+/-- `inMathlibRef` is
+* `none` at initialization time;
+* `some true` if the `header` linter has already discovered that the current file
+  is imported in `Mathlib.lean`;
+* `some false` if the `header` linter has already discovered that the current file
+  is *not* imported in `Mathlib.lean`.
+-/
+initialize inMathlibRef : IO.Ref (Option Bool) ← IO.mkRef none
+
 /--
 The "header" style linter checks that a file starts with
 ```
@@ -290,9 +299,17 @@ def duplicateImportsCheck (imports : Array Syntax)  : CommandElabM Unit := do
 @[inherit_doc Mathlib.Linter.linter.style.header]
 def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
   let mainModule ← getMainModule
+  let inMathlib? := ← match ← inMathlibRef.get with
+    | some d => return d
+    | none => do
+      let val ← isInMathlib mainModule
+      -- We store the answer to the question "is this file in `Mathlib.lean`?" in `inMathlibRef`
+      -- to avoid recomputing its value on every command. This is a performance optimisation.
+      inMathlibRef.set (some val)
+      return val
   -- The linter skips files not imported in `Mathlib.lean`, to avoid linting "scratch files".
-  -- However, it is active in the test file `MathlibTest.Header` for the linter itself.
-  unless (← isInMathlib mainModule) || mainModule == `MathlibTest.Header do return
+  -- It is however active in the test file `MathlibTest.Header` for the linter itself.
+  unless inMathlib? || mainModule == `MathlibTest.Header do return
   unless Linter.getLinterValue linter.style.header (← getOptions) do
     return
   if (← get).messages.hasErrors then