coprime_two_left

Mathlib.Data.Nat.Prime.Basic

URI: https://scilib.ai/kg/mathlib#Nat.coprime_two_left

English

Coprime(2,n) if and only if n is odd.

Русский

Взаимно простые с 2 тогда, когда n нечётно.

LaTeX

$$$$ \gcd(2,n) = 1 \iff \text{Odd}(n). $$$$

Lean4

@[simp]
theorem coprime_two_left : Coprime 2 n ↔ Odd n := by
  rw [prime_two.coprime_iff_not_dvd, ← not_even_iff_odd, even_iff_two_dvd]

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

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

Разделы

Аффилиация

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