English
If P holds for units, zero and prime powers, and P respects coprime products, then P holds for any finite product of prime powers.
Русский
Если P верно для единиц, нуля и степеней простых, и P сохраняет произведения взаимно простых элементов, то P верно для любого конечного произведения степеней простых.
LaTeX
$$$P(\\prod_{p \\in s} p^{i(p)})$ under the stated hypotheses$$
Lean4
/-- If `P` holds for `0`, units and powers of primes,
and `P x ∧ P y` for coprime `x, y` implies `P (x * y)`,
then `P` holds on all `a : α`. -/
@[elab_as_elim]
theorem induction_on_coprime {P : α → Prop} (a : α) (h0 : P 0) (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 a :=
by
letI := Classical.decEq α
have P_of_associated : ∀ {x y}, Associated x y → P x → P y :=
by
rintro x y ⟨u, rfl⟩ hx
exact hcp (fun p _ hpx => isUnit_of_dvd_unit hpx u.isUnit) hx (h1 u.isUnit)
by_cases ha0 : a = 0
· rwa [ha0]
haveI : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
letI : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
refine P_of_associated (prod_normalizedFactors ha0) ?_
rw [← (normalizedFactors a).map_id, Finset.prod_multiset_map_count]
refine induction_on_prime_power _ _ ?_ ?_ @h1 @hpr @hcp <;> simp only [Multiset.mem_toFinset]
· apply prime_of_normalized_factor
· apply normalizedFactors_eq_of_dvd
