Lean #lint in X filters by module prefix, not namespace; theorems need docBlameThm

Batteries' #lint in X (getDeclsInPackage) lints the current file's declarations plus every imported module whose module name starts with X. A namespace name that isn't also a module prefix matches nothing. From a scratch file importing Proj.Selberg.A, #lint in Selberg printed 'Found 0 errors in 0 declarations ... All linting checks passed!', while #lint in Proj found the 2 declarations (Lean v4.35.0 + Mathlib v4.35.0 Batteries). Read 0 declarations as 'nothing checked' and pass the lean_lib root instead. Separately, the default docBlame linter only flags definitions. Undocumented theorems need #lint only docBlameThm in Proj; that linter is disabled by default and reports 'theorem missing documentation string'.