chore(ring_theory/unique_factorization_domain): fix some lemma names (#…

…4765)

Fixes names of some lemmas that were erroneously renamed with find-and-replace
Changes some constructor names to use dot notation

Names replaced:
`exists_prime_of_factor` -> `exists_prime_factors`
`wf_dvd_monoid_of_exists_prime_of_factor` -> `wf_dvd_monoid.of_exists_prime_factors`
`irreducible_iff_prime_of_exists_prime_of_factor` -> `irreducible_iff_prime_of_exists_prime_factors`
`unique_factorization_monoid_of_exists_prime_of_factor` -> `unique_factorization_monoid.of_exists_prime_factors`
`unique_factorization_monoid_iff_exists_prime_of_factor` -> `unique_factorization_monoid.iff_exists_prime_factors`
`irreducible_iff_prime_of_exists_unique_irreducible_of_factor` -> `irreducible_iff_prime_of_exists_unique_irreducible_factors`
`unique_factorization_monoid.of_exists_unique_irreducible_of_factor` -> `unique_factorization_monoid.of_exists_unique_irreducible_factors`
`no_factors_of_no_prime_of_factor` -> `no_factors_of_no_prime_factors`
`dvd_of_dvd_mul_left_of_no_prime_of_factor` -> `dvd_of_dvd_mul_left_of_no_prime_factors`
`dvd_of_dvd_mul_right_of_no_prime_of_factor` -> `dvd_of_dvd_mul_right_of_no_prime_factors`

src/ring_theory/discrete_valuation_ring.lean

@@ -175,7 +175,7 @@ See `discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization`. -/
 theorem ufd : unique_factorization_monoid R :=
 let p := classical.some hR in
 let spec := classical.some_spec hR in
-unique_factorization_monoid_of_exists_prime_of_factor $ λ x hx,
+unique_factorization_monoid.of_exists_prime_factors $ λ x hx,
 begin
   use multiset.repeat p (classical.some (spec.2 hx)),
   split,

src/ring_theory/polynomial/rational_root.lean

@@ -74,7 +74,7 @@ begin
     { obtain ⟨u, hu⟩ := (f.is_unit_denom_of_num_eq_zero hr).pow p.nat_degree,
       rw ←hu at this,
       exact units.dvd_mul_right.mp this },
-    { refine dvd_of_dvd_mul_left_of_no_prime_of_factor hr _ this,
+    { refine dvd_of_dvd_mul_left_of_no_prime_factors hr _ this,
       intros q dvd_num dvd_denom_pow hq,
       apply hq.not_unit,
       exact f.num_denom_reduced r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow) } },
@@ -93,7 +93,7 @@ theorem denom_dvd_of_is_root {p : polynomial A} {r : f.codomain} (hr : aeval r p
   (f.denom r : A) ∣ p.leading_coeff :=
 begin
   suffices : (f.denom r : A) ∣ p.leading_coeff * f.num r ^ p.nat_degree,
-  { refine dvd_of_dvd_mul_left_of_no_prime_of_factor
+  { refine dvd_of_dvd_mul_left_of_no_prime_factors
       (mem_non_zero_divisors_iff_ne_zero.mp (f.denom r).2) _ this,
     intros q dvd_denom dvd_num_pow hq,
     apply hq.not_unit,

src/ring_theory/unique_factorization_domain.lean

@@ -156,17 +156,16 @@ Each element (except zero) is non-uniquely represented as a multiset
 of prime factors.
 
 To define a UFD using the definition in terms of multisets
-of irreducible factors, use the definition `of_unique_irreducible_factorization`
+of irreducible factors, use the definition `of_exists_unique_irreducible_factors`
 
 To define a UFD using the definition in terms of multisets
-of prime factors, use the definition `of_exists_prime_factorization`
+of prime factors, use the definition `of_exists_prime_factors`
 
 -/
 class unique_factorization_monoid (α : Type*) [comm_cancel_monoid_with_zero α] extends wf_dvd_monoid α :
   Prop :=
 (irreducible_iff_prime : ∀ {a : α}, irreducible a ↔ prime a)
 
-
 instance ufm_of_gcd_of_wf_dvd_monoid [nontrivial α] [comm_cancel_monoid_with_zero α]
   [wf_dvd_monoid α] [gcd_monoid α] : unique_factorization_monoid α :=
 { irreducible_iff_prime := λ _, gcd_monoid.irreducible_iff_prime
@@ -183,7 +182,7 @@ end prio
 namespace unique_factorization_monoid
 variables [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α]
 
-theorem exists_prime_of_factor (a : α) : a ≠ 0 →
+theorem exists_prime_factors (a : α) : a ≠ 0 →
   ∃ f : multiset α, (∀b ∈ f, prime b) ∧ f.prod ~ᵤ a :=
 by { simp_rw ← unique_factorization_monoid.irreducible_iff_prime,
      apply wf_dvd_monoid.exists_factors a }
@@ -274,14 +273,14 @@ begin
   exact ⟨associated.symm ⟨u, hu⟩, rfl⟩,
 end
 
-section exists_prime_of_factor
+section exists_prime_factors
 
 variables [comm_cancel_monoid_with_zero α]
 variables (pf : ∀ (a : α), a ≠ 0 → ∃ f : multiset α, (∀b ∈ f, prime b) ∧ f.prod ~ᵤ a)
 
 include pf
 
-lemma wf_dvd_monoid_of_exists_prime_of_factor : wf_dvd_monoid α :=
+lemma wf_dvd_monoid.of_exists_prime_factors : wf_dvd_monoid α :=
 ⟨begin
   classical,
   apply rel_hom.well_founded (rel_hom.mk _ _) (with_top.well_founded_lt nat.lt_wf),
@@ -313,7 +312,7 @@ lemma wf_dvd_monoid_of_exists_prime_of_factor : wf_dvd_monoid α :=
       apply (classical.some_spec (pf _ _)).2.symm, } }
 end⟩
 
-lemma irreducible_iff_prime_of_exists_prime_of_factor {p : α} : irreducible p ↔ prime p :=
+lemma irreducible_iff_prime_of_exists_prime_factors {p : α} : irreducible p ↔ prime p :=
 begin
   by_cases hp0 : p = 0,
   { simp [hp0] },
@@ -324,20 +323,20 @@ begin
   exact hf.1 q (multiset.mem_cons_self _ _)
 end
 
-theorem unique_factorization_monoid_of_exists_prime_of_factor :
+theorem unique_factorization_monoid.of_exists_prime_factors :
   unique_factorization_monoid α :=
-{ irreducible_iff_prime := λ _, irreducible_iff_prime_of_exists_prime_of_factor pf,
-  .. wf_dvd_monoid_of_exists_prime_of_factor pf }
+{ irreducible_iff_prime := λ _, irreducible_iff_prime_of_exists_prime_factors pf,
+  .. wf_dvd_monoid.of_exists_prime_factors pf }
 
-end exists_prime_of_factor
+end exists_prime_factors
 
-theorem unique_factorization_monoid_iff_exists_prime_of_factor [comm_cancel_monoid_with_zero α] :
+theorem unique_factorization_monoid.iff_exists_prime_factors [comm_cancel_monoid_with_zero α] :
   unique_factorization_monoid α ↔
     (∀ (a : α), a ≠ 0 → ∃ f : multiset α, (∀b ∈ f, prime b) ∧ f.prod ~ᵤ a) :=
-⟨λ h, @unique_factorization_monoid.exists_prime_of_factor _ _ h,
-  unique_factorization_monoid_of_exists_prime_of_factor⟩
+⟨λ h, @unique_factorization_monoid.exists_prime_factors _ _ h,
+  unique_factorization_monoid.of_exists_prime_factors⟩
 
-theorem irreducible_iff_prime_of_exists_unique_irreducible_of_factor [comm_cancel_monoid_with_zero α]
+theorem irreducible_iff_prime_of_exists_unique_irreducible_factors [comm_cancel_monoid_with_zero α]
   (eif : ∀ (a : α), a ≠ 0 → ∃ f : multiset α, (∀b ∈ f, irreducible b) ∧ f.prod ~ᵤ a)
   (uif : ∀ (f g : multiset α),
   (∀ x ∈ f, irreducible x) → (∀ x ∈ g, irreducible x) → f.prod ~ᵤ g.prod → multiset.rel associated f g)
@@ -378,28 +377,28 @@ theorem irreducible_iff_prime_of_exists_unique_irreducible_of_factor [comm_cance
               (multiset.dvd_prod hqb))
         end⟩, irreducible_of_prime⟩
 
-theorem unique_factorization_monoid.of_exists_unique_irreducible_of_factor
+theorem unique_factorization_monoid.of_exists_unique_irreducible_factors
   [comm_cancel_monoid_with_zero α]
   (eif : ∀ (a : α), a ≠ 0 → ∃ f : multiset α, (∀b ∈ f, irreducible b) ∧ f.prod ~ᵤ a)
   (uif : ∀ (f g : multiset α),
   (∀ x ∈ f, irreducible x) → (∀ x ∈ g, irreducible x) → f.prod ~ᵤ g.prod → multiset.rel associated f g) :
   unique_factorization_monoid α :=
-unique_factorization_monoid_of_exists_prime_of_factor (by
+unique_factorization_monoid.of_exists_prime_factors (by
   { convert eif,
-    simp_rw irreducible_iff_prime_of_exists_unique_irreducible_of_factor eif uif })
+    simp_rw irreducible_iff_prime_of_exists_unique_irreducible_factors eif uif })
 
 namespace unique_factorization_monoid
 variables [comm_cancel_monoid_with_zero α] [decidable_eq α] [nontrivial α] [normalization_monoid α]
 variables [unique_factorization_monoid α]
 
 /-- Noncomputably determines the multiset of prime factors. -/
 noncomputable def factors (a : α) : multiset α := if h : a = 0 then 0 else
-multiset.map normalize $ classical.some (unique_factorization_monoid.exists_prime_of_factor a h)
+multiset.map normalize $ classical.some (unique_factorization_monoid.exists_prime_factors a h)
 
 theorem factors_prod {a : α} (ane0 : a ≠ 0) : associated (factors a).prod a :=
 begin
   rw [factors, dif_neg ane0],
-  refine associated.trans _ (classical.some_spec (exists_prime_of_factor a ane0)).2,
+  refine associated.trans _ (classical.some_spec (exists_prime_factors a ane0)).2,
   rw [← associates.mk_eq_mk_iff_associated, ← associates.prod_mk, ← associates.prod_mk,
       multiset.map_map],
   congr' 2,
@@ -413,7 +412,7 @@ begin
   split_ifs with ane0, { simp },
   intros x hx, rcases multiset.mem_map.1 hx with ⟨y, ⟨hy, rfl⟩⟩,
   rw prime_iff_of_associated (normalize_associated),
-  exact (classical.some_spec (unique_factorization_monoid.exists_prime_of_factor a ane0)).1 y hy,
+  exact (classical.some_spec (unique_factorization_monoid.exists_prime_factors a ane0)).1 y hy,
 end
 
 theorem irreducible_of_factor {a : α} : ∀ (x : α), x ∈ factors a → irreducible x :=
@@ -462,7 +461,7 @@ namespace unique_factorization_monoid
 
 variables {R : Type*} [comm_cancel_monoid_with_zero R] [unique_factorization_monoid R]
 
-lemma no_factors_of_no_prime_of_factor {a b : R} (ha : a ≠ 0)
+lemma no_factors_of_no_prime_factors {a b : R} (ha : a ≠ 0)
   (h : (∀ {d}, d ∣ a → d ∣ b → ¬ prime d)) : ∀ {d}, d ∣ a → d ∣ b → is_unit d :=
 λ d, induction_on_prime d
   (by { simp only [zero_dvd_iff], intros, contradiction })
@@ -472,15 +471,15 @@ lemma no_factors_of_no_prime_of_factor {a b : R} (ha : a ≠ 0)
 
 /-- Euclid's lemma: if `a ∣ b * c` and `a` and `c` have no common prime factors, `a ∣ b`.
 Compare `is_coprime.dvd_of_dvd_mul_left`. -/
-lemma dvd_of_dvd_mul_left_of_no_prime_of_factor {a b c : R} (ha : a ≠ 0) :
+lemma dvd_of_dvd_mul_left_of_no_prime_factors {a b c : R} (ha : a ≠ 0) :
   (∀ {d}, d ∣ a → d ∣ c → ¬ prime d) → a ∣ b * c → a ∣ b :=
 begin
   refine induction_on_prime c _ _ _,
   { intro no_factors,
     simp only [dvd_zero, mul_zero, forall_prop_of_true],
     haveI := classical.prop_decidable,
     exact is_unit_iff_forall_dvd.mp
-      (no_factors_of_no_prime_of_factor ha @no_factors (dvd_refl a) (dvd_zero a)) _ },
+      (no_factors_of_no_prime_factors ha @no_factors (dvd_refl a) (dvd_zero a)) _ },
   { rintros _ ⟨x, rfl⟩ _ a_dvd_bx,
     apply units.dvd_mul_right.mp a_dvd_bx },
   { intros c p hc hp ih no_factors a_dvd_bpc,
@@ -492,9 +491,9 @@ end
 
 /-- Euclid's lemma: if `a ∣ b * c` and `a` and `b` have no common prime factors, `a ∣ c`.
 Compare `is_coprime.dvd_of_dvd_mul_right`. -/
-lemma dvd_of_dvd_mul_right_of_no_prime_of_factor {a b c : R} (ha : a ≠ 0)
+lemma dvd_of_dvd_mul_right_of_no_prime_factors {a b c : R} (ha : a ≠ 0)
   (no_factors : ∀ {d}, d ∣ a → d ∣ b → ¬ prime d) : a ∣ b * c → a ∣ c :=
-by simpa [mul_comm b c] using dvd_of_dvd_mul_left_of_no_prime_of_factor ha @no_factors
+by simpa [mul_comm b c] using dvd_of_dvd_mul_left_of_no_prime_factors ha @no_factors
 
 /-- If `a ≠ 0, b` are elements of a unique factorization domain, then dividing
 out their common factor `c'` gives `a'` and `b'` with no factors in common. -/