mathlib

8f5fd269 - feat(data/nat/factorization): bijection between positive nats and finsupps over primes (#11440)

feat(data/nat/factorization): bijection between positive nats and finsupps over primes (#11440) Proof that for any finsupp `f : ℕ →₀ ℕ` whose support is in the primes, `f = (f.prod pow).factorization`, and hence that the positive natural numbers are bijective with finsupps `ℕ →₀ ℕ` with support in the primes.