bodd

Mathlib.Data.Nat.Bits

URI: https://scilib.ai/kg/mathlib#Nat.bodd

English

bod d n returns true exactly when n is odd.

Русский

bod d n возвращает true тогда и только тогда, когда n нечетно.

LaTeX

$$$\mathrm{bodd}(n) = \mathrm{true} \iff \mathrm{Odd}(n)$$$

Lean4

/-- `bodd n` returns `true` if `n` is odd -/
def bodd (n : ℕ) : Bool :=
  (boddDiv2 n).1

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

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

Разделы

Аффилиация

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