gcd_image — Mathlib

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 [*]

Похожие утверждения