even_xor'_odd

Mathlib.Algebra.Ring.Int.Parity

URI: https://scilib.ai/kg/mathlib#Int.even_xor'_odd

English

For every integer n, exactly one of n is even or n is odd holds.

Русский

Для любого целого числа n верно: либо n четное, либо нечетное, но не оба одновременно.

LaTeX

$$$(n \equiv 0 \pmod{2}) \oplus (n \equiv 1 \pmod{2})$$$

Lean4

theorem even_xor'_odd (n : ℤ) : Xor' (Even n) (Odd n) := by grind

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

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

Разделы

Аффилиация

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