lcm — Mathlib

English

For a finite set s and a function f, the lcm of s with f is defined as the fold of lcm over s starting from 1.

Русский

Для конечного множества s и функции f наименьшее общее кратное определяется как свертывание lcm по s начиная с единицы.

LaTeX

$$$$ \\mathrm{lcm}(s,f) = \\mathrm{fold}_{s}(\\operatorname{lcm}, 1, f). $$$$

Lean4

/-- Least common multiple of a finite set -/
def lcm (s : Finset β) (f : β → α) : α :=
  s.fold GCDMonoid.lcm 1 f

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