mathlib

3c87882b - feat(number_theory/arithmetic_function): map a multiplicative function across a product (#14180)