normalize_lcm

Mathlib.Algebra.GCDMonoid.Finset

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

English

Normalizing the lcm of a finite set f does not change the value.

Русский

Нормализация НОК конечного множества не изменяет его значение.

LaTeX

$$$\operatorname{normalize}\bigl(s.lcm f\bigr) = s.lcm f$$$

Lean4

@[local simp] -- This will later be provable by other `simp` lemmas.

theorem normalize_lcm : normalize (s.lcm f) = s.lcm f := by simp [lcm_def]

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

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

Разделы

Аффилиация

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