mod_two_add_add_odd_mod_two

Mathlib.Algebra.Ring.Parity

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

English

If n is odd, then m mod 2 + (m+n) mod 2 = 1.

Русский

Если n нечетно, то сумма остатков по mod 2 остаётся равной 1.

LaTeX

$$$\\forall m \\in \\mathbb{N}, \\forall n \\in \\mathbb{N}, \\mathrm{Odd}(n) \\Rightarrow m \\bmod 2 + (m+n) \\bmod 2 = 1$$$

Lean4

theorem mod_two_add_add_odd_mod_two (m : ℕ) {n : ℕ} (hn : Odd n) : m % 2 + (m + n) % 2 = 1 := by grind

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

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

Разделы

Аффилиация

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