four_dvd_add_or_sub_of_odd

Mathlib.Algebra.Ring.Int.Parity

URI: https://scilib.ai/kg/mathlib#Int.four_dvd_add_or_sub_of_odd

English

If a and b are odd, then either a + b or a − b is divisible by 4.

Русский

Если a и b нечётны, то либо a + b, либо a − b делится на 4.

LaTeX

$$$4 \mid a + b \\lor 4 \mid a - b$$$

Lean4

theorem four_dvd_add_or_sub_of_odd {a b : ℤ} (ha : Odd a) (hb : Odd b) : 4 ∣ a + b ∨ 4 ∣ a - b := by grind

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

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

Разделы

Аффилиация

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