English
If s is nonempty, there exists a function g on s such that f(b) = s.gcd f · g(b) for all b ∈ s and s.gcd g = 1.
Русский
Если s непусто, существует функция g на s такая, что f(b) = s.gcd f · g(b) для всех b ∈ s и s.gcd g = 1.
LaTeX
$$$\\exists g : \\beta \\to \\alpha,\\ (\\forall b \\in s,\\ f(b) = s.gcd\\ f \\cdot g(b)) \\land s.gcd\\ g = 1$$$
Lean4
theorem extract_gcd (f : β → α) (hs : s.Nonempty) : ∃ g : β → α, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1 := by
classical
by_cases h : ∀ x ∈ s, f x = (0 : α)
· refine ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], ?_⟩
rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]
· choose g' hg using @gcd_dvd _ _ _ _ s f
push_neg at h
refine ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ ?_, extract_gcd' f _ h fun b hb ↦ ?_⟩
· simp only [hb, hg, dite_true]
rw [dif_pos hb, hg hb]
