map_prime_pow_mul — Mathlib

English

If f is multiplicative on coprime arguments, p ∉ s is prime, then f(p^e · m) = f(p^e) · f(m) for m ∈ factoredNumbers(s).

Русский

Если f умножима на coprime аргументы, p ∉ s и p простое, то f(p^e · m) = f(p^e) · f(m) при m ∈ factoredNumbers(s).

LaTeX

$$f (p^e * m) = f(p^e) * f(m)$$

Lean4

/-- If `f : ℕ → F` is multiplicative on coprime arguments, `p ∉ s` is a prime and `m`
is `s`-factored, then `f (p^e * m) = f (p^e) * f m`. -/
theorem map_prime_pow_mul {F : Type*} [Mul F] {f : ℕ → F} (hmul : ∀ {m n}, Coprime m n → f (m * n) = f m * f n)
    {s : Finset ℕ} {p : ℕ} (hp : p.Prime) (hs : p ∉ s) (e : ℕ) {m : factoredNumbers s} :
    f (p ^ e * m) = f (p ^ e) * f m :=
  hmul <| Coprime.pow_left _ <| hp.factoredNumbers_coprime hs <| Subtype.mem m

Похожие утверждения