feat(algebra/divisibility): generalise basic facts to semigroups (#12325

)




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/divisibility.lean

@@ -31,14 +31,14 @@ divisibility, divides
 
 variables {α : Type*}
 
-section monoid
+section semigroup
 
-variables [monoid α] {a b c : α}
+variables [semigroup α] {a b c : α}
 
 /-- There are two possible conventions for divisibility, which coincide in a `comm_monoid`.
     This matches the convention for ordinals. -/
 @[priority 100]
-instance monoid_has_dvd : has_dvd α :=
+instance semigroup_has_dvd : has_dvd α :=
 has_dvd.mk (λ a b, ∃ c, b = a * c)
 
 -- TODO: this used to not have `c` explicit, but that seems to be important
@@ -53,12 +53,6 @@ theorem exists_eq_mul_right_of_dvd (h : a ∣ b) : ∃ c, b = a * c := h
 theorem dvd.elim {P : Prop} {a b : α} (H₁ : a ∣ b) (H₂ : ∀ c, b = a * c → P) : P :=
 exists.elim H₁ H₂
 
-@[refl, simp] theorem dvd_refl (a : α) : a ∣ a :=
-dvd.intro 1 (mul_one _)
-
-lemma dvd_rfl {a : α} : a ∣ a :=
-dvd_refl a
-
 local attribute [simp] mul_assoc mul_comm mul_left_comm
 
 @[trans] theorem dvd_trans (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
@@ -69,8 +63,6 @@ end
 
 alias dvd_trans ← has_dvd.dvd.trans
 
-theorem one_dvd (a : α) : 1 ∣ a := dvd.intro a (one_mul _)
-
 @[simp] theorem dvd_mul_right (a b : α) : a ∣ a * b := dvd.intro b rfl
 
 theorem dvd_mul_of_dvd_left (h : a ∣ b) (c : α) : a ∣ b * c :=
@@ -93,11 +85,25 @@ f.to_mul_hom.map_dvd
 
 end map_dvd
 
+end semigroup
+
+section monoid
+
+variables [monoid α]
+
+@[refl, simp] theorem dvd_refl (a : α) : a ∣ a :=
+dvd.intro 1 (mul_one _)
+
+lemma dvd_rfl {a : α} : a ∣ a :=
+dvd_refl a
+
+theorem one_dvd (a : α) : 1 ∣ a := dvd.intro a (one_mul _)
+
 end monoid
 
-section comm_monoid
+section comm_semigroup
 
-variables [comm_monoid α] {a b c : α}
+variables [comm_semigroup α] {a b c : α}
 
 theorem dvd.intro_left (c : α) (h : c * a = b) : a ∣ b :=
 dvd.intro _ (begin rewrite mul_comm at h, apply h end)
@@ -125,32 +131,38 @@ local attribute [simp] mul_assoc mul_comm mul_left_comm
 theorem mul_dvd_mul : ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
 | a ._ c ._ ⟨e, rfl⟩ ⟨f, rfl⟩ := ⟨e * f, by simp⟩
 
+theorem dvd_of_mul_left_dvd (h : a * b ∣ c) : b ∣ c :=
+dvd.elim h (λ d ceq, dvd.intro (a * d) (by simp [ceq]))
+
+end comm_semigroup
+
+section comm_monoid
+
+variables [comm_monoid α] {a b : α}
+
 theorem mul_dvd_mul_left (a : α) {b c : α} (h : b ∣ c) : a * b ∣ a * c :=
 mul_dvd_mul (dvd_refl a) h
 
 theorem mul_dvd_mul_right (h : a ∣ b) (c : α) : a * c ∣ b * c :=
 mul_dvd_mul h (dvd_refl c)
 
-theorem dvd_of_mul_left_dvd (h : a * b ∣ c) : b ∣ c :=
-dvd.elim h (λ d ceq, dvd.intro (a * d) (by simp [ceq]))
-
 end comm_monoid
 
-section monoid_with_zero
+section semigroup_with_zero
 
-variables [monoid_with_zero α] {a : α}
+variables [semigroup_with_zero α] {a : α}
 
 theorem eq_zero_of_zero_dvd (h : 0 ∣ a) : a = 0 :=
 dvd.elim h (assume c, assume H' : a = 0 * c, eq.trans H' (zero_mul c))
 
-/-- Given an element `a` of a commutative monoid with zero, there exists another element whose
+/-- Given an element `a` of a commutative semigroup with zero, there exists another element whose
     product with zero equals `a` iff `a` equals zero. -/
 @[simp] lemma zero_dvd_iff : 0 ∣ a ↔ a = 0 :=
-⟨eq_zero_of_zero_dvd, λ h, by rw h⟩
+⟨eq_zero_of_zero_dvd, λ h, by { rw h, use 0, simp, }⟩
 
 @[simp] theorem dvd_zero (a : α) : a ∣ 0 := dvd.intro 0 (by simp)
 
-end monoid_with_zero
+end semigroup_with_zero
 
 /-- Given two elements `b`, `c` of a `cancel_monoid_with_zero` and a nonzero element `a`,
  `a*b` divides `a*c` iff `b` divides `c`. -/

src/algebra/gcd_monoid/basic.lean

@@ -557,9 +557,11 @@ begin
       mul_dvd_mul_iff_left h1, mul_dvd_mul_iff_right h2, and_comm] }
 end
 
-lemma dvd_lcm_left [gcd_monoid α] (a b : α) : a ∣ lcm a b := (lcm_dvd_iff.1 dvd_rfl).1
+lemma dvd_lcm_left [gcd_monoid α] (a b : α) : a ∣ lcm a b :=
+(lcm_dvd_iff.1 (dvd_refl (lcm a b))).1
 
-lemma dvd_lcm_right [gcd_monoid α] (a b : α) : b ∣ lcm a b := (lcm_dvd_iff.1 dvd_rfl).2
+lemma dvd_lcm_right [gcd_monoid α] (a b : α) : b ∣ lcm a b :=
+(lcm_dvd_iff.1 (dvd_refl (lcm a b))).2
 
 lemma lcm_dvd [gcd_monoid α] {a b c : α} (hab : a ∣ b) (hcb : c ∣ b) : lcm a c ∣ b :=
 lcm_dvd_iff.2 ⟨hab, hcb⟩

src/number_theory/padics/ring_homs.lean

@@ -378,7 +378,7 @@ begin
   { rw zero_pow hc0,
     simp only [sub_zero, zmod.cast_zero, mul_zero],
     rw unit_coeff_spec hc',
-    exact (dvd_pow_self _ hc0.ne').mul_left _ }
+    exact (dvd_pow_self (p : ℤ_[p]) hc0.ne').mul_left _, },
 end
 
 attribute [irreducible] appr