exists_eq_two_pow_mul_odd — Mathlib

English

Every nonzero natural number can be written as n = 2^k · m with m odd.

Русский

Каждое не нулевое натуральное число можно записать как n = 2^k · m, где m нечетно.

LaTeX

$$$$ \exists k,m\in\mathbb{N},\ \text{Odd}(m) \land n = 2^{k} \cdot m.$$$$

Lean4

/-- Any nonzero natural number is the product of an odd part `m` and a power of
two `2 ^ k`. -/
theorem exists_eq_two_pow_mul_odd {n : ℕ} (hn : n ≠ 0) : ∃ k m : ℕ, Odd m ∧ n = 2 ^ k * m :=
  let ⟨k, m, hm, hn⟩ := exists_eq_pow_mul_and_not_dvd hn 2 (succ_ne_self 1)
  ⟨k, m, not_even_iff_odd.1 (mt Even.two_dvd hm), hn⟩

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