even_add_one

Mathlib.Algebra.Group.Int.Even

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

English

For any integer n, n+1 is even if and only if n is not even.

Русский

Для любого целого числа n число n+1 чётно тогда и только тогда, когда n нечётно.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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