mathlib3

427e5b59 - feat(data/nat/factorization): Evaluating a multiplicative function over prime power divisors (#11167)

feat(data/nat/factorization): Evaluating a multiplicative function over prime power divisors (#11167) For any multiplicative function `f` with `f 1 = 1` and any `n > 0`, we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n`. Also provides an alternative version that swaps the `0 < n` condition for an extra `f 0 = 1` condition, as suggested by @ericrbg. This allows a very simple proof that `n.factorization.prod pow = n`