English
If f maps p^i to (f p)^i for primes p and is multiplicative on coprime products, then f is multiplicative on all products of primes.
Русский
Если f отображает p^i ↦ (f p)^i на простых p и ассоциативно умножается на coprime-продукты, то f умножаемо на любые произведения простых.
LaTeX
$$$f(\\prod_{p\\in s} p^{i(p)+j(p)}) = f(\\prod_{p\\in s} p^{i(p)})\\, f(\\prod_{p\\in s} p^{j(p)})$$$
Lean4
/-- If `P` holds for units and powers of primes,
and `P x ∧ P y` for coprime `x, y` implies `P (x * y)`,
then `P` holds on a product of powers of distinct primes. -/
@[elab_as_elim]
theorem induction_on_prime_power {P : α → Prop} (s : Finset α) (i : α → ℕ) (is_prime : ∀ p ∈ s, Prime p)
(is_coprime : ∀ᵉ (p ∈ s) (q ∈ s), p ∣ q → p = q) (h1 : ∀ {x}, IsUnit x → P x)
(hpr : ∀ {p} (i : ℕ), Prime p → P (p ^ i)) (hcp : ∀ {x y}, IsRelPrime x y → P x → P y → P (x * y)) :
P (∏ p ∈ s, p ^ i p) := by
letI := Classical.decEq α
induction s using Finset.induction_on with
| empty => simpa using h1 isUnit_one
| insert p f' hpf' ih =>
rw [Finset.prod_insert hpf']
exact
hcp (prime_pow_coprime_prod_of_coprime_insert i p hpf' is_prime is_coprime)
(hpr (i p) (is_prime _ (Finset.mem_insert_self _ _)))
(ih (fun q hq => is_prime _ (Finset.mem_insert_of_mem hq)) fun q hq q' hq' =>
is_coprime _ (Finset.mem_insert_of_mem hq) _ (Finset.mem_insert_of_mem hq'))
