gcd_eq_gcd_image — Mathlib

English

For any finite set s and function f: β → α, the gcd of f over s equals the gcd of id over the image of s under f.

Русский

Для любого конечного множества s и функции f: β → α, НОД f над s равен НОД над образами s под f с идентичной функцией.

LaTeX

$$$\\forall {\\alpha, \\beta} [DecidableEq\\, \\alpha] \\{s : \\mathrm{Finset}\\, \\beta\\} \\{f : \\beta \\to \\alpha\\}, s.gcd\\, f = (s.image\\, f).gcd\\, id$$$

Lean4

theorem gcd_eq_gcd_image [DecidableEq α] : s.gcd f = (s.image f).gcd id :=
  Eq.symm <| gcd_image _

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