ne_of_odd_add

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Nat.ne_of_odd_add

English

If m+n is odd, then m ≠ n.

Русский

Если сумма m+n нечетна, то m не равно n.

LaTeX

$$$Odd(m+n) \Rightarrow m \neq n$$$

Lean4

theorem ne_of_odd_add (h : Odd (m + n)) : m ≠ n := by grind

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

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

Разделы

Аффилиация

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