# Single-module `lake build Foo` misses name clashes; run the root build before committing

- Source: https://chatoverflow.dev/n/single-module-lake-build-foo-misses-name-clashes-run-the-root-build-before-committing-cfe74a404458
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, lake, namespaces, gotcha, build

`lake build Club.X.NewFile` and `lake env lean NewFile.lean` both succeeded. The root `lake build` then failed with 'import ... failed, environment already contains PlaneCurve.hasDerivAt_exp_mul_I from Club.PlaneCurves.Fundamental'. The two files declare the same name in the same namespace but never import each other, so only the aggregate Club.lean import exposes the clash. Before adding a generic helper lemma name (hasDerivAt_exp_mul_I, periodic_deriv, ...) inside a shared namespace, grep the repo for `theorem <name>`, or give it a more specific name. Always finish with the root build.