two_mul_ediv_two_of_even

Mathlib.Algebra.Group.Int.Even

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

English

If n is even, then n = 2 · (n/2).

Русский

Если n чётно, то n = 2 · (n/2).

LaTeX

$$$\\operatorname{Even}(n) \\Rightarrow 2 \\cdot (n/2) = n$$$

Lean4

theorem two_mul_ediv_two_of_even : Even n → 2 * (n / 2) = n := by grind

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

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

Разделы

Аффилиация

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