feat(algebra/squarefree): a squarefree element of a UFM divides a pow…

…er iff it divides (#5037)

Proves that if `x, y` are elements of a UFM such that `squarefree x`, then `x | y ^ n` iff `x | y`.

src/algebra/squarefree.lean

@@ -86,9 +86,9 @@ end multiplicity
 
 namespace unique_factorization_monoid
 variables [comm_cancel_monoid_with_zero R] [nontrivial R] [unique_factorization_monoid R]
-variables [normalization_monoid R] [decidable_eq R]
+variables [normalization_monoid R]
 
-lemma squarefree_iff_nodup_factors {x : R} (x0 : x ≠ 0) :
+lemma squarefree_iff_nodup_factors [decidable_eq R] {x : R} (x0 : x ≠ 0) :
   squarefree x ↔ multiset.nodup (factors x) :=
 begin
   have drel : decidable_rel (has_dvd.dvd : R → R → Prop),
@@ -115,6 +115,20 @@ begin
     assumption_mod_cast }
 end
 
+lemma dvd_pow_iff_dvd_of_squarefree {x y : R} {n : ℕ} (hsq : squarefree x) (h0 : n ≠ 0) :
+  x ∣ y ^ n ↔ x ∣ y :=
+begin
+  classical,
+  by_cases hx : x = 0,
+  { simp [hx, pow_eq_zero_iff (nat.pos_of_ne_zero h0)] },
+  by_cases hy : y = 0,
+  { simp [hy, zero_pow (nat.pos_of_ne_zero h0)] },
+  refine ⟨λ h, _, λ h, dvd_pow h h0⟩,
+  rw [dvd_iff_factors_le_factors hx (pow_ne_zero n hy), factors_pow,
+    ((squarefree_iff_nodup_factors hx).1 hsq).le_nsmul_iff_le h0] at h,
+  rwa dvd_iff_factors_le_factors hx hy,
+end
+
 end unique_factorization_monoid
 
 namespace nat

src/data/multiset/basic.lean

@@ -848,6 +848,13 @@ quotient.induction_on s $ λ l,
 lemma dvd_prod [comm_monoid α] {a : α} {s : multiset α} : a ∈ s → a ∣ s.prod :=
 quotient.induction_on s (λ l a h, by simpa using list.dvd_prod h) a
 
+lemma prod_dvd_prod [comm_monoid α] {s t : multiset α} (h : s ≤ t) :
+  s.prod ∣ t.prod :=
+begin
+  rcases multiset.le_iff_exists_add.1 h with ⟨z, rfl⟩,
+  simp,
+end
+
 theorem prod_eq_zero_iff [comm_cancel_monoid_with_zero α] [nontrivial α]
   {s : multiset α} :
   s.prod = 0 ↔ (0 : α) ∈ s :=
@@ -1797,6 +1804,17 @@ instance : semilattice_sup_bot (multiset α) :=
 
 end
 
+@[simp]
+lemma mem_nsmul {a : α} {s : multiset α} {n : ℕ} (h0 : n ≠ 0) :
+  a ∈ n •ℕ s ↔ a ∈ s :=
+begin
+  classical,
+  cases n,
+  { exfalso, apply h0 rfl },
+  rw [← not_iff_not, ← count_eq_zero, ← count_eq_zero],
+  simp [h0],
+end
+
 /- relator -/
 
 section rel

src/data/multiset/erase_dup.lean

@@ -75,4 +75,26 @@ by simp [nodup_ext]
 theorem erase_dup_map_erase_dup_eq [decidable_eq β] (f : α → β) (s : multiset α) :
   erase_dup (map f (erase_dup s)) = erase_dup (map f s) := by simp [erase_dup_ext]
 
+@[simp]
+lemma erase_dup_nsmul {s : multiset α} {n : ℕ} (h0 : n ≠ 0) :
+  (n •ℕ s).erase_dup = s.erase_dup :=
+begin
+  ext a,
+  by_cases h : a ∈ s;
+  simp [h,h0]
+end
+
+lemma nodup.le_erase_dup_iff_le {s t : multiset α} (hno : s.nodup) :
+  s ≤ t.erase_dup ↔ s ≤ t :=
+by simp [le_erase_dup, hno]
+
 end multiset
+
+lemma multiset.nodup.le_nsmul_iff_le {α : Type*} {s t : multiset α}
+  {n : ℕ} (h : s.nodup) (hn : n ≠ 0) :
+  s ≤ n •ℕ t ↔ s ≤ t :=
+begin
+  classical,
+  rw [← h.le_erase_dup_iff_le, iff.comm, ← h.le_erase_dup_iff_le],
+  simp [hn]
+end

src/ring_theory/unique_factorization_domain.lean

@@ -426,6 +426,8 @@ have multiset.rel associated (p ::ₘ factors b) (factors a),
           (associated.symm (factors_prod hb0))),
 multiset.exists_mem_of_rel_of_mem this (by simp)
 
+@[simp] lemma factors_zero : factors (0 : α) = 0 := dif_pos rfl
+
 @[simp] lemma factors_one : factors (1 : α) = 0 :=
 begin
   rw ← multiset.rel_zero_right,
@@ -459,6 +461,26 @@ begin
       (factors_prod (mul_ne_zero hx hy)).symm, }
 end
 
+@[simp] lemma factors_pow {x : α} (n : ℕ) :
+  factors (x ^ n) = n •ℕ factors x :=
+begin
+  induction n with n ih,
+  { simp },
+  by_cases h0 : x = 0,
+  { simp [h0, zero_pow n.succ_pos, smul_zero] },
+  rw [pow_succ, succ_nsmul, factors_mul h0 (pow_ne_zero _ h0), ih],
+end
+
+lemma dvd_iff_factors_le_factors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
+  x ∣ y ↔ factors x ≤ factors y :=
+begin
+  split,
+  { rintro ⟨c, rfl⟩,
+    simp [hx, right_ne_zero_of_mul hy] },
+  { rw [← dvd_iff_dvd_of_rel_left (factors_prod hx), ← dvd_iff_dvd_of_rel_right (factors_prod hy)],
+    apply multiset.prod_dvd_prod }
+end
+
 end unique_factorization_monoid
 
 namespace unique_factorization_monoid