English
If there exist f, g: β → α and hs: ∃ x ∈ s with f(x) ≠ 0, and hg: ∀ b ∈ s, f(b) = s.gcd f · g(b), then s.gcd g = 1.
Русский
Если существуют f, g: β → α и существуют элементы s, such что ∃ x ∈ s, f(x) ≠ 0, и для всех b ∈ s выполняется f(b) = s.gcd f · g(b), то gcd над g равен 1.
LaTeX
$$$(\\exists x, x \\in s \\land f(x) \\neq 0) \\land (\\forall b \\in s,\\ f(b) = s.gcd\\ f \\cdot g(b)) \\Rightarrow s.gcd\\ g = 1$$$
Lean4
theorem extract_gcd' (f g : β → α) (hs : ∃ x, x ∈ s ∧ f x ≠ 0) (hg : ∀ b ∈ s, f b = s.gcd f * g b) : s.gcd g = 1 :=
((@mul_right_eq_self₀ _ _ (s.gcd f) _).1 <| by
conv_lhs => rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]).resolve_right <|
by
contrapose! hs
exact gcd_eq_zero_iff.1 hs
