sub_even

Mathlib.Algebra.Ring.Parity

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

English

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

Русский

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

LaTeX

$$$\forall m,n \in \mathbb{N},\, n \le m \land \mathrm{Odd}(m) \land \mathrm{Even}(n) \Rightarrow \mathrm{Odd}(m-n).$$$

Lean4

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

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

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

Разделы

Аффилиация

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