gcd_dvd_left

Mathlib.Algebra.EuclideanDomain.Basic

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

English

gcd(a,b) divides a.

Русский

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

LaTeX

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

Lean4

theorem gcd_dvd_left (a b : R) : gcd a b ∣ a :=
  (gcd_dvd a b).left

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

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

Разделы

Аффилиация

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