succ_mod_two_add_mod_two

Mathlib.Algebra.Ring.Parity

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

English

For every m there exists k such that m = 2k or m = 2k+1.

Русский

Для каждого m существует k, такое что m = 2k или m = 2k+1.

LaTeX

$$$\\forall m \\in \\mathbb{N}, \\exists k \\in \\mathbb{N}, m = 2k \\lor m = 2k + 1$$$

Lean4

@[simp]
theorem succ_mod_two_add_mod_two (m : ℕ) : (m + 1) % 2 + m % 2 = 1 := by cutsat

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

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

Разделы

Аффилиация

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