refactor(ring_theory/associated): rename associated_elements

Author: digama0

ring_theory/associated_elements.lean renamed to ring_theory/associated.lean

@@ -15,11 +15,6 @@ def is_unit [monoid α] (a : α) : Prop := ∃u:units α, a = u
 @[simp] theorem not_is_unit_zero [nonzero_comm_ring α] : ¬ is_unit (0 : α)
 | ⟨⟨a, b, hab, hba⟩, rfl⟩ := have 0 * b = 1, from hab, by simpa using this
 
-@[simp] theorem is_unit_nat {n : ℕ} : is_unit n ↔ n = 1 :=
-iff.intro
-  (assume ⟨u, hu⟩, match n, u, hu, nat.units_eq_one u with _, _, rfl, rfl := rfl end)
-  (assume h, h.symm ▸ ⟨1, rfl⟩)
-
 @[simp] theorem is_unit_one [monoid α] : is_unit (1:α) := ⟨1, rfl⟩
 
 theorem units.is_unit_of_mul_one [comm_monoid α] (a b : α) (h : a * b = 1) : is_unit a :=
@@ -32,12 +27,29 @@ iff.intro
     by rwa [mul_assoc, units.mul_inv, mul_one] at this)
   (assume ⟨v, hv⟩, hv.symm ▸ ⟨v * u, (units.mul_coe v u).symm⟩)
 
+theorem is_unit_iff_dvd_one {α} [comm_semiring α] {x : α} : is_unit x ↔ x ∣ 1 :=
+⟨by rintro ⟨u, rfl⟩; exact ⟨_, u.mul_inv.symm⟩,
+ λ ⟨y, h⟩, ⟨⟨x, y, h.symm, by rw [h, mul_comm]⟩, rfl⟩⟩
+
+theorem is_unit_iff_forall_dvd {α} [comm_semiring α] {x : α} :
+  is_unit x ↔ ∀ y, x ∣ y :=
+is_unit_iff_dvd_one.trans ⟨λ h y, dvd.trans h (one_dvd _), λ h, h _⟩
+
+theorem is_unit_of_dvd_unit {α} [comm_semiring α] {x y : α}
+  (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
+is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
+
+@[simp] theorem is_unit_nat {n : ℕ} : is_unit n ↔ n = 1 :=
+iff.intro
+  (assume ⟨u, hu⟩, match n, u, hu, nat.units_eq_one u with _, _, rfl, rfl := rfl end)
+  (assume h, h.symm ▸ ⟨1, rfl⟩)
+
 /-- `irreducible p` states that `p` is non-unit and only factors into units.
 
 We explicitly avoid stating that `p` is non-zero, this would require a semiring. Assuming only a
 monoid allows us to reuse irreducible for associated elements.
 -/
-def irreducible [monoid α] (p : α) : Prop :=
+@[class] def irreducible [monoid α] (p : α) : Prop :=
 ¬ is_unit p ∧ ∀a b, p = a * b → is_unit a ∨ is_unit b
 
 @[simp] theorem not_irreducible_one [monoid α] : ¬ irreducible (1 : α) :=
@@ -47,6 +59,21 @@ by simp [irreducible]
 | ⟨hn0, h⟩ := have is_unit (0:α) ∨ is_unit (0:α), from h 0 0 ((mul_zero 0).symm),
   this.elim hn0 hn0
 
+theorem of_irreducible_mul {α} [monoid α] {x y : α} :
+  irreducible (x * y) → is_unit x ∨ is_unit y
+| ⟨_, h⟩ := h _ _ rfl
+
+theorem irreducible_or_factor {α} [monoid α] (x : α) (h : ¬ is_unit x) :
+  irreducible x ∨ ∃ a b, ¬ is_unit a ∧ ¬ is_unit b ∧ a * b = x :=
+begin
+  haveI := classical.dec,
+  refine or_iff_not_imp_right.2 (λ H, _),
+  simp [h, irreducible] at H ⊢,
+  refine λ a b h, classical.by_contradiction $ λ o, _,
+  simp [not_or_distrib] at o,
+  exact H _ o.1 _ o.2 h.symm
+end
+
 theorem irreducible_iff_nat_prime : ∀(a : ℕ), irreducible a ↔ nat.prime a
 | 0 := by simp [nat.not_prime_zero]
 | 1 := by simp [nat.prime, one_lt_two]

ring_theory/unique_factorization_domain.lean

@@ -7,7 +7,7 @@ Theory of unique factorization domains.
 
 @TODO: setup the complete lattice structure on `factor_set`.
 -/
-import ring_theory.associated_elements algebra.gcd_domain
+import ring_theory.associated algebra.gcd_domain
 
 variables {α : Type*}
 local infix ` ~ᵤ ` : 50 := associated