even_xor_odd

Mathlib.Algebra.Ring.Parity

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

English

For every n, n is even or n is odd (exclusive).

Русский

Для каждого n верно: либо n чётно, либо n нечётно (исключающе).

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\mathrm{Even}(n) \\oplus \\mathrm{Odd}(n)$$$

Lean4

theorem even_xor_odd (n : ℕ) : Xor' (Even n) (Odd n) := by grind

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

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

Разделы

Аффилиация

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