mathlib

28031a80 - feat(number_theory/factorization): evaluating arithmetic functions at prime powers (#13817)