English
The gcd of f over s equals the gcd of f restricted to those x in s with f(x) ≠ 0.
Русский
НОД f над s равен НОД f на подмножестве элементов s, для которых f(x) ≠ 0.
LaTeX
$$$s.gcd\\, f = (\\{x \\in s \\mid f(x) \\neq 0\\}).gcd\\, f$$$
Lean4
theorem gcd_eq_gcd_filter_ne_zero [DecidablePred fun x : β ↦ f x = 0] : s.gcd f = {x ∈ s | f x ≠ 0}.gcd f := by
classical
trans ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
· rw [filter_union_filter_neg_eq]
rw [gcd_union]
refine Eq.trans (?_ : _ = GCDMonoid.gcd (0 : α) ?_) (?_ : GCDMonoid.gcd (0 : α) _ = _)
· exact gcd ({x ∈ s | f x ≠ 0}) f
· refine congr (congr rfl <| s.induction_on ?_ ?_) (by simp)
· simp
· intro a s _ h
rw [filter_insert]
split_ifs with h1 <;> simp [h, h1]
simp only [gcd_zero_left, normalize_gcd]
