normalize_gcd

Mathlib.Algebra.GCDMonoid.Basic

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

English

In a NormalizedGCDMonoid α, for all a,b we have normalize(gcd(a,b)) = gcd(a,b).

Русский

В нормализованном gcd-монойде α для любых a,b выполняется normalize(gcd(a,b)) = gcd(a,b).

LaTeX

$$$$ \\forall a,b, \\operatorname{normalize}(\\gcd(a,b)) = \\gcd(a,b) $$$$

Lean4

@[simp]
theorem normalize_gcd [NormalizedGCDMonoid α] : ∀ a b : α, normalize (gcd a b) = gcd a b :=
  NormalizedGCDMonoid.normalize_gcd

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

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

Разделы

Аффилиация

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