odd_one

Mathlib.Algebra.Ring.Parity

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

English

1 is odd in any semiring.

Русский

1 в любом полугруппе нечётно.

LaTeX

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

Lean4

@[simp]
theorem odd_one : Odd (1 : α) :=
  ⟨0, (zero_add _).symm.trans (congr_arg (· + (1 : α)) (mul_zero _).symm)⟩

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

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

Разделы

Аффилиация

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