lcm_singleton

Mathlib.Algebra.GCDMonoid.Multiset

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

English

LCM of a singleton {a} equals the normal form of a.

Русский

LCM одиночного множества {a} равен нормализованному a.

LaTeX

$$$\\mathrm{lcm}({a}) = \\operatorname{normalize}(a)$$$

Lean4

@[simp]
theorem lcm_singleton {a : α} : ({ a } : Multiset α).lcm = normalize a :=
  (fold_singleton _ _ _).trans <| lcm_one_right _

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

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

Разделы

Аффилиация

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