Commit 2022-03-24 10:12 e6c6f006

View on Github →

feat(number_theory/arithmetic_function): The moebius function is multiplicative (#12796) A fundamental property of the moebius function is that it is multiplicative, which allows many facts about Euler products to be expressed

Estimated changes

Modified src/algebra/squarefree.lean

added theorem nat.squarefree_mul

added theorem squarefree.ne_zero

added theorem squarefree.of_mul_left

added theorem squarefree.of_mul_right

Modified src/number_theory/arithmetic_function.lean

added theorem nat.arithmetic_function.is_multiplicative.iff_ne_zero

added theorem nat.arithmetic_function.is_multiplicative_moebius