From 915d8709421a6201e92e40bb1b402e27965390e5 Mon Sep 17 00:00:00 2001 From: Ralf Stephan Date: Thu, 27 Jun 2024 00:05:43 +0000 Subject: [PATCH] feat(Nat/Factorization): add `exists_eq_two_pow_mul_odd` (#14166) Any nonzero natural number is the product of an odd part `m` and a power of two `2 ^ k`. This is a trivial consequence of the existing `exists_eq_pow_mul_and_not_dvd`, but performs a convenient restatement in terms of `Odd`. Needed by #14049. Co-authored-by: Thomas Browning --- Mathlib/Data/Nat/Factorization/Basic.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 734dba8823e6f..574f9a87e30c5 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -534,6 +534,13 @@ theorem exists_eq_pow_mul_and_not_dvd {n : ℕ} (hn : n ≠ 0) (p : ℕ) (hp : p ⟨_, a', h₂, h₁⟩ #align nat.exists_eq_pow_mul_and_not_dvd Nat.exists_eq_pow_mul_and_not_dvd +/-- 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, odd_iff_not_even.mpr (mt Even.two_dvd hm), hn⟩ + theorem dvd_iff_div_factorization_eq_tsub {d n : ℕ} (hd : d ≠ 0) (hdn : d ≤ n) : d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization := by refine ⟨factorization_div, ?_⟩