normalize_lcm

Mathlib.Algebra.GCDMonoid.Multiset

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

English

Normalizing the lcm of a multiset yields the same multiset lcm.

Русский

Нормализация НОД множества не меняет его LCM.

LaTeX

$$$\\forall s,\\ \\mathrm{normalize}(s.lcm) = s.lcm$$$

Lean4

@[simp]
theorem normalize_lcm (s : Multiset α) : normalize s.lcm = s.lcm :=
  Multiset.induction_on s (by simp) fun a s _ ↦ by simp

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

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

Разделы

Аффилиация

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