gcd_singleton

Mathlib.Algebra.GCDMonoid.Finset

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

English

The gcd over singleton {b} equals the normalization of f(b).

Русский

НОД над одиночкой {b} равен нормализации f(b).

LaTeX

$$$\operatorname{gcd}({b}) f = \operatorname{normalize}(f(b))$$$

Lean4

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

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

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

Разделы

Аффилиация

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