gcd_singleton

Mathlib.Algebra.GCDMonoid.Multiset

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

English

The gcd of a singleton multiset {a} is the normalization of a: gcd({a}) = normalize(a).

Русский

НОД множества вида {a} равен нормализации a: gcd({a}) = normalize(a).

LaTeX

$$$\{a\}.\mathrm{gcd} = \mathrm{normalize}(a)$$$

Lean4

@[simp]
theorem gcd_singleton {a : α} : ({ a } : Multiset α).gcd = normalize a :=
  (fold_singleton _ _ _).trans <| gcd_zero_right _

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

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

Разделы

Аффилиация

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