feat(number_theory/divisors): add prod_div_divisors and `sum_div_di…

…visors` (#12087)

Adds lemma `prod_div_divisors : ∏ d in n.divisors, f (n/d) = n.divisors.prod f` and `sum_div_divisors`.

Also proves `image_div_divisors_eq_divisors : image (λ (x : ℕ), n / x) n.divisors = n.divisors`
and `div_eq_iff_eq_of_dvd_dvd : n / x = n / y ↔ x = y` (where `n ≠ 0` and `x ∣ n` and `y ∣ n`)

src/data/nat/basic.lean

@@ -876,6 +876,18 @@ begin
   exact nat.lt_succ_self _,
 end
 
+lemma div_eq_iff_eq_of_dvd_dvd {n x y : ℕ} (hn : n ≠ 0) (hx : x ∣ n) (hy : y ∣ n) :
+  n / x = n / y ↔ x = y :=
+begin
+  split,
+  { intros h,
+    rw ←mul_right_inj' hn,
+    apply nat.eq_mul_of_div_eq_left (dvd_mul_of_dvd_left hy x),
+    rw [eq_comm, mul_comm, nat.mul_div_assoc _ hy],
+    exact nat.eq_mul_of_div_eq_right hx h },
+  { intros h, rw h },
+end
+
 /-! ### `mod`, `dvd` -/
 
 lemma div_add_mod (m k : ℕ) : k * (m / k) + m % k = m :=

src/number_theory/divisors.lean

@@ -435,4 +435,34 @@ begin
     simpa [hn, hn.ne', mem_factors] using and_comm (prime q) (q ∣ n) }
 end
 
+@[simp]
+lemma image_div_divisors_eq_divisors (n : ℕ) : image (λ (x : ℕ), n / x) n.divisors = n.divisors :=
+begin
+  by_cases hn : n = 0, { simp [hn] },
+  ext,
+  split,
+  { rw mem_image,
+    rintros ⟨x, hx1, hx2⟩,
+    rw mem_divisors at *,
+    refine ⟨_,hn⟩,
+    rw ←hx2,
+    exact div_dvd_of_dvd hx1.1 },
+  { rw [mem_divisors, mem_image],
+    rintros ⟨h1, -⟩,
+    exact ⟨n/a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩,
+           nat.div_div_self h1 (pos_iff_ne_zero.mpr hn)⟩ },
+end
+
+@[simp, to_additive sum_div_divisors]
+lemma prod_div_divisors {α : Type*} [comm_monoid α] (n : ℕ) (f : ℕ → α) :
+  ∏ d in n.divisors, f (n/d) = n.divisors.prod f :=
+begin
+  by_cases hn : n = 0, { simp [hn] },
+  rw ←prod_image,
+  { exact prod_congr (image_div_divisors_eq_divisors n) (by simp) },
+  { intros x hx y hy h,
+    rw mem_divisors at hx hy,
+    exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h }
+end
+
 end nat