normalize_gcd

Mathlib.Algebra.GCDMonoid.Multiset

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

English

Normalizing the gcd does not change it: normalize(gcd(s)) = gcd(s).

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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