gcd_one_left

Mathlib.Algebra.EuclideanDomain.Basic

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

English

gcd(1,a) = 1 for any a in a Euclidean domain.

Русский

gcd(1,a) = 1 для любого a в евклидовом кольце.

LaTeX

$$$ gcd\,1\,a = 1 $$$

Lean4

@[simp]
theorem gcd_one_left (a : R) : gcd 1 a = 1 :=
  gcd_eq_left.2 (one_dvd _)

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

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

Разделы

Аффилиация

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