sub_even

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Odd.sub_even

English

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

Русский

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

LaTeX

$$$\operatorname{Odd}(a) \land \operatorname{Even}(b) \rightarrow \operatorname{Odd}(a-b)$$$

Lean4

theorem sub_even (ha : Odd a) (hb : Even b) : Odd (a - b) := by rw [sub_eq_add_neg]; exact ha.add_even hb.neg

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

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

Разделы

Аффилиация

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