English
For any nonzero multiset s, there exists t such that s = t.map(s.gcd * ·) and t.gcd = 1.
Русский
Для любого ненулевого мультисетa существует t such that s = t.map(s.gcd * ·) и t.gcd = 1.
LaTeX
$$$\exists t\ :\ \operatorname{Multiset}(\alpha),\ s = t.map( s.\mathrm{gcd} * \\cdot ) \land t.\mathrm{gcd} = 1$$$
Lean4
theorem extract_gcd (s : Multiset α) (hs : s ≠ 0) : ∃ t : Multiset α, s = t.map (s.gcd * ·) ∧ t.gcd = 1 := by
classical
by_cases h : ∀ x ∈ s, x = (0 : α)
· use replicate (card s) 1
rw [map_replicate, eq_replicate, mul_one, s.gcd_eq_zero_iff.2 h, ← nsmul_singleton, ← gcd_dedup,
dedup_nsmul (card_pos.2 hs).ne', dedup_singleton, gcd_singleton]
exact ⟨⟨rfl, h⟩, normalize_one⟩
· choose f hf using @gcd_dvd _ _ _ s
push_neg at h
refine ⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩ <;>
· rw [map_pmap]
conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
congr with (x hx)
rw [id, ← hf hx]
