Mobius_Function_is_Multiplicative
Provedmobius-functionmultiplicative-functionsproofwiki
The Möbius function is multiplicative: if gcd(m,n)=1 then μ(mn) = μ(m)μ(n).
Preamble
import Mathlib.NumberTheory.ArithmeticFunction
Formal statement
theorem Mobius_Function_is_Multiplicative (m n : ℕ) (hmn : Nat.Coprime m n) : ArithmeticFunction.moebius (m * n) = ArithmeticFunction.moebius m * ArithmeticFunction.moebius n := by sorry
Source