English
Two multiplicative functions f,g are equal iff they agree on all prime powers p^i.
Русский
Два умножаемых по определению f и g равны тогда и только тогда, когда они совпадают на всех простых степенях p^i.
LaTeX
$$$f=g \iff \forall p,i,\ Nat.Prime(p) \Rightarrow f(p^i)=g(p^i)$$$
Lean4
/-- Two multiplicative functions `f` and `g` are equal if and only if
they agree on prime powers -/
theorem eq_iff_eq_on_prime_powers [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative)
(g : ArithmeticFunction R) (hg : g.IsMultiplicative) : f = g ↔ ∀ p i : ℕ, Nat.Prime p → f (p ^ i) = g (p ^ i) :=
by
constructor
· intro h p i _
rw [h]
intro h
ext n
by_cases hn : n = 0
· rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]
rw [multiplicative_factorization f hf hn, multiplicative_factorization g hg hn]
exact Finset.prod_congr rfl fun p hp ↦ h p _ (Nat.prime_of_mem_primeFactors hp)
