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

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.