gcd_dvd_right

Mathlib.Algebra.EuclideanDomain.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.gcd_dvd_right

English

gcd(a,b) divides b.

Русский

gcd(a,b) делит b.

LaTeX

$$$ gcd\,a\,b \mid b $$$

Lean4

theorem gcd_dvd_right (a b : R) : gcd a b ∣ b :=
  (gcd_dvd a b).right

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

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

Разделы

Аффилиация

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