one_coprime

Mathlib.Data.PNat.Prime

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem one_coprime {n : ℕ+} : (1 : ℕ+).Coprime n :=
  one_gcd

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

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

Разделы

Аффилиация

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