Commit 2024-11-21 17:01 2d53f5f7
View on Github →feat(Data/Nat/Factorization/PrimePow): add equivalence Primes × ℕ ≃ PrimePowers (#19335) This is part of the series of PRs leading to Dirichlet's Theorem on primes in AP. See here on Zulip.
feat(Data/Nat/Factorization/PrimePow): add equivalence Primes × ℕ ≃ PrimePowers (#19335) This is part of the series of PRs leading to Dirichlet's Theorem on primes in AP. See here on Zulip.