setGcd — Mathlib

English

The gcd of a set s is defined as the nonnegative generator of the ideal of integers generated by s.

Русский

НОД множества s определяется как неотрицательный генератор идеала в \\mathbb{Z}, порождаемого изображением s.

LaTeX

$$$\\mathrm{setGcd}(s) = \\operatorname{natAbs}\\big(\\operatorname{generator}(\\operatorname{Ideal.span}(\\{\\iota(n) \\mid n \\in s\\}))\\big)$$$

Lean4

/-- The gcd of a set of natural numbers is defined to be the nonnegative generator
of the ideal of `ℤ` generated by them. -/
noncomputable def setGcd (s : Set ℕ) : ℕ :=
  (generator <| Ideal.span <| ((↑) : ℕ → ℤ) '' s).natAbs

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