Mathlib now has a definition of Dirichlet density. Merge with Mathlib and use its definition of Dirichlet density. Don't just make a bridge between its definition and yours: delete yours and use Mathlib's everywhere changing what needs to be changed.
Mathlib now has a definition of Dirichlet density. Merge with Mathlib and use its definition of Dirichlet density. Don't just make a bridge between its definition and yours: delete yours and use Mathlib's everywhere changing what needs to be changed.