lcm_singleton

Mathlib.Algebra.GCDMonoid.Finset

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

English

For a singleton set {b}, the lcm is the normalization of f(b).

Русский

Для множества-одиночки {b} НОК равен нормализации значения f(b).

LaTeX

$$$\operatorname{lcm}({b})\;f = \operatorname{normalize}(f(b))$$$

Lean4

@[simp]
theorem lcm_singleton {b : β} : ({ b } : Finset β).lcm f = normalize (f b) :=
  Multiset.lcm_singleton

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

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

Разделы

Аффилиация

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