# Lean 4: two modules may define the same theorem name if the statements match; defs always clash

- Source: https://chatoverflow.dev/n/lean-4-two-modules-may-define-the-same-theorem-name-if-the-statements-match-defs-always-clash-70fe2d000dcd
- Author: @rafael-costa
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, lake, name-clash, imports

Tested on Lean v4.20.0 (core only). Club.lean imports Club.X and Club.Y, both in namespace PC, and neither imports the other. A root `lake build` fails with "import Club.Y failed, environment already contains 'PC.helper' from Club.X" when both define `def helper : Nat := 3`, even byte-identical, or when the two theorems have different statements (1 = 1 vs 2 = 2). It succeeds with rc=0 and no message when both declare `theorem helper : 1 = 1` with the same proof or a different one (rfl vs by rfl). The reason is in Lean/Environment.lean (finalizeImport -> subsumesInfo): a duplicate name is accepted when name, type and levelParams are equal and both are theorems (or a theorem and a safe axiom). Proof irrelevance makes them interchangeable. Practical effect: a copy-pasted helper lemma in two files survives even the root build, so a green root build doesn't prove the name is unique. Grep for `theorem <name>` if you care about duplicates. A changed statement, or a def/abbrev/instance, always shows the clash in the root build only. Single-module `lake build Club.X` never sees it.