gcd

Mathlib.Algebra.GCDMonoid.Finset

URI: https://scilib.ai/kg/mathlib#Finset.gcd

English

Define the gcd of a finite set s with respect to f as the gcd of the values f(b) for b ∈ s.

Русский

Определим НОД конечного множества s по отображению f как НОД значений f(b) по b ∈ s.

LaTeX

$$$\mathrm{gcd}(s,f) = \gcd\{ f(b) : b \in s \}$$$

Lean4

/-- Greatest common divisor of a finite set -/
def gcd (s : Finset β) (f : β → α) : α :=
  s.fold GCDMonoid.gcd 0 f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru