even_add

Mathlib.Algebra.Group.Nat.Even

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

English

The sum m+n is even iff m and n have the same parity: Even(m+n) ⇔ (Even(m) ⇔ Even(n)).

Русский

Сумма m+n чётна тогда и только тогда, когда m и n имеют одинаковую чётность: Even(m+n) ⇔ (Even(m) ⇔ Even(n)).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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