two_not_dvd_two_mul_add_one

Mathlib.Algebra.Group.Int.Even

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

English

For all n, 2 ∤ (2n+1).

Русский

Для любого n числа 2 не делит (2n+1).

LaTeX

$$$\forall n\in \mathbb{Z},\ \neg 2 \mid (2\,n+1)$$$

Lean4

theorem two_not_dvd_two_mul_add_one (n : ℤ) : ¬2 ∣ 2 * n + 1 := by grind

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

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

Разделы

Аффилиация

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