Theorems · Theorem · number theory

ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers

∀ {R : Type u_1} [inst : CommMonoidWithZero R] (f : ArithmeticFunction R),
  f.IsMultiplicative →
    ∀ (g : ArithmeticFunction R), g.IsMultiplicative → (f = g ↔ ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i))

Two multiplicative functions f and g are equal if and only if they agree on prime powers

Defined in

Mathlib.NumberTheory.ArithmeticFunction.Defs

Cited by

0 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZero