not_odd_iff_even

Mathlib.Algebra.Ring.Parity

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

English

For all natural numbers n, not Odd n iff Even n.

Русский

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

LaTeX

$$$\forall n, \neg \operatorname{Odd}(n) \iff \operatorname{Even}(n)$$$

Lean4

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

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

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

Разделы

Аффилиация

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