odd_add_self_one'

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#odd_add_self_one'

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem odd_add_self_one' : Odd (a + (a + 1)) := by simp [← add_assoc]

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

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

Разделы

Аффилиация

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