feat(data/nat/totient): add lemma totient_dvd_of_dvd (#15642)

Adds `totient_dvd_of_dvd (h : a ∣ b) : φ a ∣ φ b`.  This is Theorem 2.5(d) in Apostol (1976) Introduction to Analytic Number Theory.

Author: stuart-presnell

src/data/finsupp/basic.lean

@@ -1535,6 +1535,18 @@ have ∀ {f1 f2 : α →₀ M}, disjoint f1.support f2.support →
 by simp_rw [← this hd, ← this hd.symm,
   add_comm (f2 _), finsupp.prod, support_add_eq hd, prod_union hd, add_apply]
 
+lemma prod_dvd_prod_of_subset_of_dvd [add_comm_monoid M] [comm_monoid N]
+  {f1 f2 : α →₀ M} {g1 g2 : α → M → N} (h1 : f1.support ⊆ f2.support)
+  (h2 : ∀ (a : α), a ∈ f1.support → g1 a (f1 a) ∣ g2 a (f2 a)) :
+  f1.prod g1 ∣ f2.prod g2 :=
+begin
+  simp only [finsupp.prod, finsupp.prod_mul],
+  rw [←sdiff_union_of_subset h1, prod_union sdiff_disjoint],
+  apply dvd_mul_of_dvd_right,
+  apply prod_dvd_prod_of_dvd,
+  exact h2,
+end
+
 section map_range
 
 section equiv

src/data/nat/totient.lean

@@ -336,6 +336,19 @@ begin
   apply mul_le_mul_left' (nat.totient_le d),
 end
 
+lemma totient_dvd_of_dvd {a b : ℕ} (h : a ∣ b) : φ a ∣ φ b :=
+begin
+  rcases eq_or_ne a 0 with rfl | ha0, { simp [zero_dvd_iff.1 h] },
+  rcases eq_or_ne b 0 with rfl | hb0, { simp },
+  have hab' : a.factorization.support ⊆ b.factorization.support,
+  { intro p,
+    simp only [support_factorization, list.mem_to_finset],
+    apply factors_subset_of_dvd h hb0 },
+  rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0],
+  refine finsupp.prod_dvd_prod_of_subset_of_dvd hab' (λ p hp, mul_dvd_mul _ dvd_rfl),
+  exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1),
+end
+
 lemma totient_mul_of_prime_of_dvd {p n : ℕ} (hp : p.prime) (h : p ∣ n) :
   (p * n).totient = p * n.totient :=
 begin