associated_gcd_gcd

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#IsBezout.associated_gcd_gcd

← MathLib Explorer

English

Associated(IsBezout.gcd(x,y), GCDMonoid.gcd(x,y))

Русский

Ассоциированы gcd, как из IsBezout, так и из GCDMonoid.

LaTeX

$$$\\\\mathrm{Associated}(\\\\gcd x y, \\\\mathrm{GCDMonoid}.gcd x y)$$$

Lean4

theorem associated_gcd_gcd [IsDomain R] [GCDMonoid R] : Associated (IsBezout.gcd x y) (GCDMonoid.gcd x y) :=
  gcd_greatest_associated (gcd_dvd_left _ _) (gcd_dvd_right _ _) (fun _ => dvd_gcd)

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

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

Разделы

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

Аффилиация

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