two_dvd_mul_add_one

Mathlib.Algebra.Ring.Int.Parity

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

English

For every integer k, 2 divides k(k+1).

Русский

Для целого k число k(k+1) делится на 2.

LaTeX

$$$2 \mid k(k+1)$$$

Lean4

theorem two_dvd_mul_add_one (k : ℤ) : 2 ∣ k * (k + 1) :=
  even_iff_two_dvd.mp (even_mul_succ_self k)

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

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

Разделы

Аффилиация

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