normalize_gcd

Mathlib.Algebra.GCDMonoid.Finset

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

English

Normalization leaves gcd unchanged: normalize(s.gcd f) = s.gcd f.

Русский

Нормализация не изменяет gcd: normalize(s.gcd f) = s.gcd f.

LaTeX

$$$\operatorname{normalize}(s.gcd f) = s.gcd f$$$

Lean4

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

theorem normalize_gcd : normalize (s.gcd f) = s.gcd f := by simp [gcd_def]

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

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

Разделы

Аффилиация

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