sub_odd

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Nat.Even.sub_odd

English

Let m,n ∈ ℕ with n ≤ m. If m is even and n is odd, then m − n is odd.

Русский

Пусть m,n ∈ ℕ с n ≤ m. Если m четно и n нечетно, то m − n нечетно.

LaTeX

$$$n \le m \Rightarrow \mathrm{Even}(m) \land \mathrm{Odd}(n) \Rightarrow \mathrm{Odd}(m-n).$$$

Lean4

theorem sub_odd (h : n ≤ m) (hm : Even m) (hn : Odd n) : Odd (m - n) := by grind

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

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

Разделы

Аффилиация

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