English
For a function g: γ → β and a Finset s of γ, the gcd of f over the image s.image g equals the gcd of f ∘ g over s.
Русский
Для функции g: γ → β и конечного множества s ⊆ γ, НОД над образа s.image g совпадает с НОД над f ∘ g на s.
LaTeX
$$$\\forall [\\text{DecidableEq }\\beta] \\{g : \\gamma \\to \\beta\\} (s : \\mathrm{Finset}\\, \\gamma), \\ (s.image\\, g).gcd\\, f = s.gcd\\, (f \\circ g)$$$
Lean4
theorem gcd_image [DecidableEq β] {g : γ → β} (s : Finset γ) : (s.image g).gcd f = s.gcd (f ∘ g) := by
classical induction s using Finset.induction <;> simp [*]