add_odd

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Even.add_odd

English

If a is even and b is odd, then a + b is odd.

Русский

Если a чётное, а b нечётное, то a + b нечётное.

LaTeX

$$$\\text{Even}(a) \\to \\text{Odd}(b) \\to \\text{Odd}(a+b)$$$

Lean4

theorem add_odd : Even a → Odd b → Odd (a + b) := by rintro ⟨a, rfl⟩ ⟨b, rfl⟩;
  exact ⟨a + b, by rw [mul_add, ← two_mul, add_assoc]⟩

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

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

Разделы

Аффилиация

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