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

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.