even_sub'

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Nat.even_sub'

English

If n ≤ m, then m−n is even iff (Odd m ↔ Odd n).

Русский

Если n ≤ m, то m−n чётно тогда и только тогда, когда m и n имеют одинаковый паритет.

LaTeX

$$$n \\le m \\Rightarrow (Even(m-n) \\leftrightarrow (Odd(m) \\leftrightarrow Odd(n)))$$$

Lean4

theorem even_sub' (h : n ≤ m) : Even (m - n) ↔ (Odd m ↔ Odd n) := by grind

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

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

Разделы

Аффилиация

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