not_even_iff_odd

Mathlib.Algebra.Ring.Parity

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

English

For every natural number n, n is odd if and only if n is not even.

Русский

Для любого натурального числа n верно: n нечетно тогда и только тогда, когда n не делится на 2.

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\neg \\mathrm{Even}(n) \\Leftrightarrow \\mathrm{Odd}(n)$$$

Lean4

@[simp]
theorem not_even_iff_odd : ¬Even n ↔ Odd n := by grind

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

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

Разделы

Аффилиация

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