odd_add_one_self

Mathlib.Algebra.Ring.Parity

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

English

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

Русский

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

LaTeX

$$$\operatorname{Odd}(a+1+a)$$$

Lean4

@[simp]
theorem odd_add_one_self : Odd (a + 1 + a) := by simp [add_comm _ a]

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

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

Разделы

Аффилиация

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