gcd_comm'

Mathlib.Algebra.GCDMonoid.Basic

URI: https://scilib.ai/kg/mathlib#gcd_comm'

← MathLib Explorer

English

In a gcd-monoid α, gcd(a,b) is associated with gcd(b,a).

Русский

В gcd-монойде α gcd(a,b) ассоциировано с gcd(b,a).

LaTeX

$$$$ \\operatorname{Associated}(\\gcd(a,b), \\gcd(b,a)) $$$$

Lean4

theorem gcd_comm' [GCDMonoid α] (a b : α) : Associated (gcd a b) (gcd b a) :=
  associated_of_dvd_dvd (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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