odd_iff

Mathlib.Algebra.Ring.Parity

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

English

In natural numbers, n is odd if and only if n mod 2 equals 1.

Русский

В натуральных числах n нечётно тогда, когда n mod 2 равняется 1.

LaTeX

$$$\operatorname{Odd}(n) \iff n \\% 2 = 1$$$

Lean4

@[grind =]
theorem odd_iff : Odd n ↔ n % 2 = 1 :=
  ⟨fun ⟨m, hm⟩ ↦ by cutsat, fun h ↦ ⟨n / 2, by cutsat⟩⟩

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

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

Разделы

Аффилиация

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