odd_iff_exists_bit1 — Mathlib

English

Let α be a semiring and a ∈ α. Then a is odd iff there exists b ∈ α with a = 2·b + 1.

Русский

Пусть α — полукольцо и a ∈ α. Тогда a нечётно тогда и только тогда, когда существует b ∈ α такое, что a = 2·b + 1.

LaTeX

$$$\\mathrm{Odd}(a) \\iff \\exists b:\\alpha,\\ a = 2 \\cdot b + 1$$$

Lean4

theorem odd_iff_exists_bit1 : Odd a ↔ ∃ b, a = 2 * b + 1 :=
  exists_congr fun b ↦ by rw [two_mul]

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