boddDiv2 — Mathlib

English

bod d o d n returns a pair (b, m) where b indicates whether n is odd and m = ⌊n/2⌋.

Русский

bod d o d n возвращает пару (b, m), где b указывает на нечетность n, а m = ⌊n/2⌋.

LaTeX

$$$\mathrm{boddDiv2}(n) = (\mathrm{bodd}(n), \mathrm{div2}(n))$$$

Lean4

/-- `boddDiv2 n` returns a 2-tuple of type `(Bool, Nat)` where the `Bool` value indicates whether
`n` is odd or not and the `Nat` value returns `⌊n/2⌋` -/
def boddDiv2 : ℕ → Bool × ℕ
  | 0 => (false, 0)
  | succ n =>
    match boddDiv2 n with
    | (false, m) => (true, m)
    | (true, m) => (false, succ m)

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