lcm_def

Mathlib.Algebra.GCDMonoid.Finset

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

English

The lcm of a finite set s with function f equals the lcm of the image of s under map f.

Русский

НОК конечного множества s с функцией f равен НОК образа s под отображением f.

LaTeX

$$$$ \\mathrm{lcm}(s,f) = \\mathrm{Multiset.lcm}(\\mathrm{map}(f, s . \\text{val})). $$$$

Lean4

theorem lcm_def : s.lcm f = (s.1.map f).lcm :=
  rfl

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

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

Разделы

Аффилиация

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