even_add_one

Mathlib.Algebra.Group.Nat.Even

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

English

Even(n+1) iff not Even(n).

Русский

Even(n+1) эквивалентно нечетности n.

LaTeX

$$$\operatorname{Even}(n+1) \iff \neg \operatorname{Even}(n)$$$

Lean4

@[parity_simps]
theorem even_add_one : Even (n + 1) ↔ ¬Even n := by grind

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

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

Разделы

Аффилиация

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