odd_iff

Mathlib.Algebra.Ring.Int.Parity

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

English

For any integer n, Odd n if and only if n ≡ 1 mod 2.

Русский

Для любого целого числа n нечетность эквивалентна тому, что n ≡ 1 по модулю 2.

LaTeX

$$$\text{Odd}(n) \iff n \equiv 1 \pmod{2}$$$

Lean4

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

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

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

Разделы

Аффилиация

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