feat(algebra/associated): simple lemmas and dot notation (#8770)

Introduce
* `prime.exists_mem_finset_dvd`
* `prime.not_dvd_one`

Rename
* `exists_mem_multiset_dvd_of_prime` -> `prime.exists_mem_multiset_dvd`
* `left_dvd_or_dvd_right_of_dvd_prime_mul ` ->`prime.left_dvd_or_dvd_right_of_dvd_mul`

Author: YaelDillies

archive/imo/imo2001_q6.lean

@@ -39,7 +39,7 @@ begin
     ... = (a * c + b * d) * (b ^ 2 + b * d + d ^ 2)         : by ring, },
   -- since `a*b + c*d` is prime (by assumption), it must divide `a*c + b*d` or `a*d + b*c`
   obtain (h1 : a*b + c*d ∣ a*c + b*d) | (h2 : a*c + b*d ∣ a*d + b*c) :=
-    left_dvd_or_dvd_right_of_dvd_prime_mul h0 dvd_mul,
+    h0.left_dvd_or_dvd_right_of_dvd_mul dvd_mul,
   -- in both cases, we derive a contradiction
   { have aux : 0 < a*c + b*d,         { nlinarith only [ha, hb, hc, hd] },
     have : a*b + c*d ≤ a*c + b*d,     { from int.le_of_dvd aux h1 },

src/algebra/associated.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
 -/
-import data.multiset.basic
+import algebra.big_operators.basic
 import algebra.divisibility
 import algebra.invertible
 
@@ -56,14 +56,18 @@ p ≠ 0 ∧ ¬ is_unit p ∧ (∀a b, p ∣ a * b → p ∣ a ∨ p ∣ b)
 
 namespace prime
 variables {p : α} (hp : prime p)
+include hp
 
-lemma ne_zero (hp : prime p) : p ≠ 0 :=
+lemma ne_zero : p ≠ 0 :=
 hp.1
 
-lemma not_unit (hp : prime p) : ¬ is_unit p :=
+lemma not_unit : ¬ is_unit p :=
 hp.2.1
 
-lemma ne_one (hp : prime p) : p ≠ 1 :=
+lemma not_dvd_one : ¬ p ∣ 1 :=
+mt (is_unit_of_dvd_one _) hp.not_unit
+
+lemma ne_one : p ≠ 1 :=
 λ h, hp.2.1 (h.symm ▸ is_unit_one)
 
 lemma dvd_or_dvd (hp : prime p) {a b : α} (h : p ∣ a * b) :
@@ -84,6 +88,25 @@ begin
   exact ih dvd_pow
 end
 
+lemma exists_mem_multiset_dvd {s : multiset α} :
+  p ∣ s.prod → ∃ a ∈ s, p ∣ a :=
+multiset.induction_on s (λ h, (hp.not_dvd_one h).elim) $
+λ a s ih h,
+  have p ∣ a * s.prod, by simpa using h,
+  match hp.dvd_or_dvd this with
+  | or.inl h := ⟨a, multiset.mem_cons_self a s, h⟩
+  | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
+  end
+
+lemma exists_mem_multiset_map_dvd {s : multiset β} {f : β → α} :
+  p ∣ (s.map f).prod → ∃ a ∈ s, p ∣ f a :=
+λ h, by simpa only [exists_prop, multiset.mem_map, exists_exists_and_eq_and]
+  using hp.exists_mem_multiset_dvd h
+
+lemma exists_mem_finset_dvd {s : finset β} {f : β → α} :
+  p ∣ s.prod f → ∃ i ∈ s, p ∣ f i :=
+hp.exists_mem_multiset_map_dvd
+
 end prime
 
 @[simp] lemma not_prime_zero : ¬ prime (0 : α) :=
@@ -92,22 +115,12 @@ end prime
 @[simp] lemma not_prime_one : ¬ prime (1 : α) :=
 λ h, h.not_unit is_unit_one
 
-lemma exists_mem_multiset_dvd_of_prime {s : multiset α} {p : α} (hp : prime p) :
-  p ∣ s.prod → ∃a∈s, p ∣ a :=
-multiset.induction_on s (assume h, (hp.not_unit $ is_unit_of_dvd_one _ h).elim) $
-assume a s ih h,
-  have p ∣ a * s.prod, by simpa using h,
-  match hp.dvd_or_dvd this with
-  | or.inl h := ⟨a, multiset.mem_cons_self a s, h⟩
-  | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
-  end
-
 end prime
 
-lemma left_dvd_or_dvd_right_of_dvd_prime_mul [comm_cancel_monoid_with_zero α] {a : α} :
-  ∀ {b p : α}, prime p → a ∣ p * b → p ∣ a ∨ a ∣ b :=
+lemma prime.left_dvd_or_dvd_right_of_dvd_mul [comm_cancel_monoid_with_zero α] {p : α}
+  (hp : prime p) {a b : α} : a ∣ p * b → p ∣ a ∨ a ∣ b :=
 begin
-  rintros b p hp ⟨c, hc⟩,
+  rintro ⟨c, hc⟩,
   rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with h | ⟨x, rfl⟩,
   { exact or.inl h },
   { rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc,

src/ring_theory/unique_factorization_domain.lean

@@ -548,7 +548,7 @@ begin
   { intros c p hc hp ih no_factors a_dvd_bpc,
     apply ih (λ q dvd_a dvd_c hq, no_factors dvd_a (dvd_mul_of_dvd_right dvd_c _) hq),
     rw mul_left_comm at a_dvd_bpc,
-    refine or.resolve_left (left_dvd_or_dvd_right_of_dvd_prime_mul hp a_dvd_bpc) (λ h, _),
+    refine or.resolve_left (hp.left_dvd_or_dvd_right_of_dvd_mul a_dvd_bpc) (λ h, _),
     exact no_factors h (dvd_mul_right p c) hp }
 end
 
@@ -583,7 +583,7 @@ begin
     { obtain ⟨a', b', c', coprime, rfl, rfl⟩ := ih_a a_ne_zero b,
       refine ⟨p * a', b', c', _, mul_left_comm _ _ _, rfl⟩,
       intros q q_dvd_pa' q_dvd_b',
-      cases left_dvd_or_dvd_right_of_dvd_prime_mul p_prime q_dvd_pa' with p_dvd_q q_dvd_a',
+      cases p_prime.left_dvd_or_dvd_right_of_dvd_mul q_dvd_pa' with p_dvd_q q_dvd_a',
       { have : p ∣ c' * b' := dvd_mul_of_dvd_right (p_dvd_q.trans q_dvd_b') _,
         contradiction },
       exact coprime q_dvd_a' q_dvd_b' } }