gcd_one

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.gcd_one

English

For any positive n, gcd(n,1) = 1, i.e., 1 is coprime to every positive integer.

Русский

Для любого положительного n: gcd(n,1)=1, т.е. 1 взаимно простое с любым положительным числом.

LaTeX

$$$ \gcd(n,1) = 1 $$$

Lean4

@[simp]
theorem gcd_one {n : ℕ+} : gcd n 1 = 1 := by
  rw [gcd_comm]
  apply one_gcd

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

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

Разделы

Аффилиация

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