mathlib3

14ee5e03 - feat(number_theory/arithmetic_function): add eq of multiplicative functions (#12689)

feat(number_theory/arithmetic_function): add eq of multiplicative functions (#12689) To show that two multiplicative functions are equal, it suffices to show that they are equal on prime powers. This is a commonly used strategy when two functions are known to be multiplicative (e.g., they're both Dirichlet convolutions of simpler multiplicative functions). This will be used in several ongoing commits to prove asymptotics for squarefree numbers.