English
If i ∈ s and f(i) ≠ 0, then s.gcd f divided by s.gcd f equals 1 after division of values by s.gcd f; more precisely gcd of (f j)/(s.gcd f) over j ∈ s equals 1.
Русский
Если i ∈ s и f(i) ≠ 0, то gcd элементов f(j)/s.gcd f по j ∈ s равен 1.
LaTeX
$$$\\text{has : } i \\in s \\land h(f,i) \\Rightarrow s.gcd\\ (\\lambda j, f(j)/s.gcd\\ f) = 1$$$
Lean4
/-- Given a nonempty Finset `s` and a function `f` from `s` to `ℕ`, if `d = s.gcd`,
then the `gcd` of `(f i) / d` is equal to `1`. -/
theorem gcd_div_eq_one (his : i ∈ s) (hfi : f i ≠ 0) : s.gcd (fun j ↦ f j / s.gcd f) = 1 :=
by
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨i, his⟩
refine (Finset.gcd_congr rfl fun a ha ↦ ?_).trans hg
rw [he a ha, mul_div_cancel_left₀]
exact mt Finset.gcd_eq_zero_iff.1 fun h ↦ hfi <| h i his
