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 1 a]

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

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

Разделы

Аффилиация

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