natAbs_even

Mathlib.Algebra.Ring.Int.Parity

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

English

For any integer n, natAbs(n) is even iff n is even.

Русский

Для любого целого числа n natAbs(n) чётно тогда и только тогда, когда n чётно.

LaTeX

$$$\\operatorname{Even}(n_{\\mathrm{nat}}) \\iff \\operatorname{Even}(n)$$$

Lean4

@[simp]
theorem natAbs_even : Even n.natAbs ↔ Even n := by grind

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

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

Разделы

Аффилиация

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