`dupNamespace` linter should ignore aux lemmas
urkud opened this issue · 0 comments
urkud commented
In leanprover-community/mathlib4#2244, there are several false positives because the file is named Mathlib/Algbera/Algebra/Basic.lean, so aux lemmas have Algebra.Algebra in their names.