even_sub_one

Mathlib.Algebra.Group.Int.Even

URI: https://scilib.ai/kg/mathlib#Int.even_sub_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_sub_one : Even (n - 1) ↔ ¬Even n := by grind

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

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

Разделы

Аффилиация

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