English
If two nonzero elements have the same factorization, they are associated.
Русский
Если два ненулевых элемента имеют одинаковое разложение по простым, они ассоциированы.
LaTeX
$$$a \\neq 0,\\ b \\neq 0,\\ \\text{factorization}(a) = \\text{factorization}(b) \\Rightarrow a \\sim b$$$
Lean4
/-- If `f` maps `p ^ i` to `(f p) ^ i` for primes `p`, and `f`
is multiplicative on coprime elements, then `f` is multiplicative on all products of primes. -/
theorem multiplicative_prime_power {f : α → β} (s : Finset α) (i j : α → ℕ) (is_prime : ∀ p ∈ s, Prime p)
(is_coprime : ∀ᵉ (p ∈ s) (q ∈ s), p ∣ q → p = q) (h1 : ∀ {x y}, IsUnit y → f (x * y) = f x * f y)
(hpr : ∀ {p} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) (hcp : ∀ {x y}, IsRelPrime x y → f (x * y) = f x * f y) :
f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p) :=
by
letI := Classical.decEq α
induction s using Finset.induction_on with
| empty => simpa using h1 isUnit_one
| insert p s hps ih =>
have hpr_p := is_prime _ (Finset.mem_insert_self _ _)
have hpr_s : ∀ p ∈ s, Prime p := fun p hp => is_prime _ (Finset.mem_insert_of_mem hp)
have hcp_p := fun i => prime_pow_coprime_prod_of_coprime_insert i p hps is_prime is_coprime
have hcp_s : ∀ᵉ (p ∈ s) (q ∈ s), p ∣ q → p = q := fun p hp q hq =>
is_coprime p (Finset.mem_insert_of_mem hp) q (Finset.mem_insert_of_mem hq)
rw [Finset.prod_insert hps, Finset.prod_insert hps, Finset.prod_insert hps, hcp (hcp_p _), hpr _ hpr_p,
hcp (hcp_p _), hpr _ hpr_p, hcp (hcp_p (fun p => i p + j p)), hpr _ hpr_p, ih hpr_s hcp_s, pow_add, mul_assoc,
mul_left_comm (f p ^ j p), mul_assoc]
