odd_two_mul_add_one

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#odd_two_mul_add_one

English

Let α be a semiring. For every a ∈ α, 2a+1 is odd.

Русский

Пусть α — полукольцо. Для каждого элемента a ∈ α число 2a+1 нечётно.

LaTeX

$$$\forall a\in \alpha,\ \operatorname{Odd}(2a+1)$$$

Lean4

theorem odd_two_mul_add_one (a : α) : Odd (2 * a + 1) :=
  ⟨_, rfl⟩

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

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

Разделы

Аффилиация

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