even_add

Mathlib.Algebra.Group.Int.Even

URI: https://scilib.ai/kg/mathlib#Int.even_add

English

Even(m+n) iff (Even m ↔ Even n).

Русский

Четность суммы равна нечетности обоих. Эквивалентно тому, что m и n имеют одну и ту же четность.

LaTeX

$$$\operatorname{Even}(m+n) \iff (\operatorname{Even}(m) \iff \operatorname{Even}(n))$$$

Lean4

@[parity_simps]
theorem even_add : Even (m + n) ↔ (Even m ↔ Even n) := by grind

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

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

Разделы

Аффилиация

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