diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index eb1e03de83..cb2b23f45a 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -155,3 +155,9 @@ Test files (in `tests/`) do not need copyright headers.
 ## Test Module Docstrings
 
 Every test `.lean` file must include a module docstring (`/-! ... -/`) briefly explaining what the file tests. For regression tests, reference the issue (e.g. `#13599`). Place the docstring after the `import` block, if any.
+
+## Rebasing vs PR base
+
+When asked to "rebase a PR onto X", **only change the local branch base** — never change the PR's `--base` target on GitHub unless explicitly told to.
+
+Common Lean4 case: rebasing onto `nightly-with-mathlib` is done to get a mathlib-tested snapshot for CI; the PR still targets `master`.