refactor(algebra/group_with_zero): rename lemmas to use ₀ instead of ' (

#9424)

We currently have lots of lemmas for `group_with_zero` that already have a corresponding lemma for `group`. We've dealt with name collisions so far just by adding a prime.

This PR renames these lemmas to use a `₀` suffix instead of a `'`.

In part this is out of desire to reduce our overuse of primes in mathlib names (putting the burden on users to know names, rather than relying on naming conventions).

But it may also help with a problem Daniel Selsam ran into at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mathport.20depending.20on.20mathlib. (Briefly, mathport is also adding primes to names when it encounters name collisions, and these particular primes were causing problems. There are are other potential fixes in the works, but everything helps.)




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

archive/100-theorems-list/70_perfect_numbers.lean

@@ -90,7 +90,7 @@ begin
   rcases nat.coprime.dvd_of_dvd_mul_left
     (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)) (dvd.intro _ perf) with ⟨j, rfl⟩,
   rw [← mul_assoc, mul_comm _ (mersenne _), mul_assoc] at perf,
-  have h := mul_left_cancel' (ne_of_gt (mersenne_pos (nat.succ_pos _))) perf,
+  have h := mul_left_cancel₀ (ne_of_gt (mersenne_pos (nat.succ_pos _))) perf,
   rw [sigma_one_apply, sum_divisors_eq_sum_proper_divisors_add_self, ← succ_mersenne, add_mul,
     one_mul, add_comm] at h,
   have hj := add_left_cancel h,
@@ -100,7 +100,7 @@ begin
     simp [h_1, j1] },
   { have jcon := eq.trans hj.symm h_1,
     rw [← one_mul j, ← mul_assoc, mul_one] at jcon,
-    have jcon2 := mul_right_cancel' _ jcon,
+    have jcon2 := mul_right_cancel₀ _ jcon,
     { exfalso,
       cases k,
       { apply hm,

src/algebra/algebra/bilinear.lean

@@ -131,17 +131,17 @@ variables {R A : Type*} [comm_semiring R] [ring A] [algebra R A]
 lemma lmul_left_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
   function.injective (lmul_left R x) :=
 by { letI : domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
-     exact mul_right_injective' hx }
+     exact mul_right_injective₀ hx }
 
 lemma lmul_right_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
   function.injective (lmul_right R x) :=
 by { letI : domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
-     exact mul_left_injective' hx }
+     exact mul_left_injective₀ hx }
 
 lemma lmul_injective [no_zero_divisors A] {x : A} (hx : x ≠ 0) :
   function.injective (lmul R A x) :=
 by { letI : domain A := { exists_pair_ne := ⟨x, 0, hx⟩, ..‹ring A›, ..‹no_zero_divisors A› },
-     exact mul_right_injective' hx }
+     exact mul_right_injective₀ hx }
 
 end
 

src/algebra/archimedean.lean

@@ -185,7 +185,7 @@ begin
   { use 1, simp only [pow_one], linarith, },
   rw [not_le] at y_pos,
   rcases pow_unbounded_of_one_lt (x⁻¹) (one_lt_inv y_pos hy) with ⟨q, hq⟩,
-  exact ⟨q, by rwa [inv_pow', inv_lt_inv hx (pow_pos y_pos _)] at hq⟩
+  exact ⟨q, by rwa [inv_pow₀, inv_lt_inv hx (pow_pos y_pos _)] at hq⟩
 end
 
 /-- Given `x` and `y` between `0` and `1`, `x` is between two successive powers of `y`.
@@ -197,8 +197,8 @@ begin
   rcases exists_nat_pow_near (one_le_inv_iff.2 ⟨xpos, hx⟩) (one_lt_inv_iff.2 ⟨ypos, hy⟩)
     with ⟨n, hn, h'n⟩,
   refine ⟨n, _, _⟩,
-  { rwa [inv_pow', inv_lt_inv xpos (pow_pos ypos _)] at h'n },
-  { rwa [inv_pow', inv_le_inv (pow_pos ypos _) xpos] at hn }
+  { rwa [inv_pow₀, inv_lt_inv xpos (pow_pos ypos _)] at h'n },
+  { rwa [inv_pow₀, inv_le_inv (pow_pos ypos _) xpos] at hn }
 end
 
 variables [floor_ring α]

src/algebra/associated.lean

@@ -33,7 +33,7 @@ lemma dvd_and_not_dvd_iff [comm_cancel_monoid_with_zero α] {x y : α} :
 ⟨λ ⟨⟨d, hd⟩, hyx⟩, ⟨λ hx0, by simpa [hx0] using hyx, ⟨d,
     mt is_unit_iff_dvd_one.1 (λ ⟨e, he⟩, hyx ⟨e, by rw [hd, mul_assoc, ← he, mul_one]⟩), hd⟩⟩,
   λ ⟨hx0, d, hdu, hdx⟩, ⟨⟨d, hdx⟩, λ ⟨e, he⟩, hdu (is_unit_of_dvd_one _
-    ⟨e, mul_left_cancel' hx0 $ by conv {to_lhs, rw [he, hdx]};simp [mul_assoc]⟩)⟩⟩
+    ⟨e, mul_left_cancel₀ hx0 $ by conv {to_lhs, rw [he, hdx]};simp [mul_assoc]⟩)⟩⟩
 
 lemma pow_dvd_pow_iff [comm_cancel_monoid_with_zero α]
   {x : α} {n m : ℕ} (h0 : x ≠ 0) (h1 : ¬ is_unit x) :
@@ -181,10 +181,10 @@ protected lemma prime.irreducible [comm_cancel_monoid_with_zero α] {p : α} (hp
 ⟨hp.not_unit, λ a b hab,
   (show a * b ∣ a ∨ a * b ∣ b, from hab ▸ hp.dvd_or_dvd (hab ▸ dvd_rfl)).elim
     (λ ⟨x, hx⟩, or.inr (is_unit_iff_dvd_one.2
-      ⟨x, mul_right_cancel' (show a ≠ 0, from λ h, by simp [*, prime] at *)
+      ⟨x, mul_right_cancel₀ (show a ≠ 0, from λ h, by simp [*, prime] at *)
         $ by conv {to_lhs, rw hx}; simp [mul_comm, mul_assoc, mul_left_comm]⟩))
     (λ ⟨x, hx⟩, or.inl (is_unit_iff_dvd_one.2
-      ⟨x, mul_right_cancel' (show b ≠ 0, from λ h, by simp [*, prime] at *)
+      ⟨x, mul_right_cancel₀ (show b ≠ 0, from λ h, by simp [*, prime] at *)
         $ by conv {to_lhs, rw hx}; simp [mul_comm, mul_assoc, mul_left_comm]⟩))⟩
 
 lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul [comm_cancel_monoid_with_zero α]
@@ -290,9 +290,9 @@ begin
   have hac0 : a * c ≠ 0,
   { intro con, rw [con, zero_mul] at a_eq, apply ha0 a_eq, },
   have : a * (c * d) =  a * 1 := by rw [← mul_assoc, ← a_eq, mul_one],
-  have hcd : (c * d) = 1, from mul_left_cancel' ha0 this,
+  have hcd : (c * d) = 1, from mul_left_cancel₀ ha0 this,
   have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one],
-  have hdc : d * c = 1, from mul_left_cancel' hac0 this,
+  have hdc : d * c = 1, from mul_left_cancel₀ hac0 this,
   exact ⟨⟨c, d, hcd, hdc⟩, rfl⟩
 end
 
@@ -368,7 +368,7 @@ protected lemma associated.irreducible_iff [monoid α] {p q : α} (h : p ~ᵤ q)
 lemma associated.of_mul_left [comm_cancel_monoid_with_zero α] {a b c d : α}
   (h : a * b ~ᵤ c * d) (h₁ : a ~ᵤ c) (ha : a ≠ 0) : b ~ᵤ d :=
 let ⟨u, hu⟩ := h in let ⟨v, hv⟩ := associated.symm h₁ in
-⟨u * (v : units α), mul_left_cancel' ha
+⟨u * (v : units α), mul_left_cancel₀ ha
   begin
     rw [← hv, mul_assoc c (v : α) d, mul_left_comm c, ← hu],
     simp [hv.symm, mul_assoc, mul_comm, mul_left_comm]
@@ -709,7 +709,7 @@ begin
   rintros ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h,
   rcases quotient.exact' h with ⟨u, hu⟩,
   have hu : a * (b * ↑u) = a * c, { rwa [← mul_assoc] },
-  exact quotient.sound' ⟨u, mul_left_cancel' (mt mk_eq_zero.2 ha) hu⟩
+  exact quotient.sound' ⟨u, mul_left_cancel₀ (mt mk_eq_zero.2 ha) hu⟩
 end
 
 lemma eq_of_mul_eq_mul_right :

src/algebra/big_operators/basic.lean

@@ -1316,7 +1316,7 @@ begin
   { push_neg at h,
     have h' := prod_ne_zero_iff.mpr h,
     have hf : ∀ x ∈ s, (f x)⁻¹ * f x = 1 := λ x hx, inv_mul_cancel (h x hx),
-    apply mul_right_cancel' h',
+    apply mul_right_cancel₀ h',
     simp [h, h', ← finset.prod_mul_distrib, prod_congr rfl hf] }
 end
 

src/algebra/field.lean

@@ -100,7 +100,7 @@ calc
 lemma neg_div (a b : K) : (-b) / a = - (b / a) :=
 by rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]
 
-@[field_simps] lemma neg_div' {K : Type*} [division_ring K] (a b : K) : - (b / a) = (-b) / a :=
+@[field_simps] lemma neg_div' (a b : K) : - (b / a) = (-b) / a :=
 by simp [neg_div]
 
 lemma neg_div_neg_eq (a b : K) : (-a) / (-b) = a / b :=
@@ -300,7 +300,7 @@ lemma map_ne_zero : f x ≠ 0 ↔ x ≠ 0 := f.to_monoid_with_zero_hom.map_ne_ze
 
 variables (x y)
 
-lemma map_inv : g x⁻¹ = (g x)⁻¹ := g.to_monoid_with_zero_hom.map_inv' x
+lemma map_inv : g x⁻¹ = (g x)⁻¹ := g.to_monoid_with_zero_hom.map_inv x
 
 lemma map_div : g (x / y) = g x / g y := g.to_monoid_with_zero_hom.map_div x y
 

src/algebra/gcd_monoid/basic.lean

@@ -364,7 +364,7 @@ begin
     { cases h with b hb,
       use b,
       rw mul_assoc at hb,
-      apply mul_left_cancel' h0 hb },
+      apply mul_left_cancel₀ h0 hb },
     rw ← ha,
     exact dvd_gcd_mul_of_dvd_mul H }
 end
@@ -670,13 +670,13 @@ def normalization_monoid_of_monoid_hom_right_inverse [decidable_eq α] (f : asso
     suffices : (a * b) * ↑(classical.some (associated_map_mk hinv (a * b))) =
       (a * ↑(classical.some (associated_map_mk hinv a))) *
       (b * ↑(classical.some (associated_map_mk hinv b))),
-    { apply mul_left_cancel' (mul_ne_zero ha hb) _,
+    { apply mul_left_cancel₀ (mul_ne_zero ha hb) _,
       simpa only [mul_assoc, mul_comm, mul_left_comm] using this },
     rw [map_mk_unit_aux hinv a, map_mk_unit_aux hinv (a * b), map_mk_unit_aux hinv b,
         ← monoid_hom.map_mul, associates.mk_mul_mk] },
   norm_unit_coe_units := λ u, by {
     rw [if_neg (units.ne_zero u), units.ext_iff],
-    apply mul_left_cancel' (units.ne_zero u),
+    apply mul_left_cancel₀ (units.ne_zero u),
     rw [units.mul_inv, map_mk_unit_aux hinv u,
       associates.mk_eq_mk_iff_associated.2 (associated_one_iff_is_unit.2 ⟨u, rfl⟩),
       associates.mk_one, monoid_hom.map_one] } }
@@ -742,7 +742,7 @@ let exists_gcd := λ a b, dvd_normalize_iff.2 (lcm_dvd (dvd.intro b rfl) (dvd.in
       have h := lcm_dvd (dvd.intro b rfl) (dvd.intro_left a rfl),
       rw [con, zero_dvd_iff, mul_eq_zero] at h,
       cases h; tauto },
-    apply mul_left_cancel' h0,
+    apply mul_left_cancel₀ h0,
     refine trans _ (classical.some_spec (exists_gcd a b)),
     conv_lhs { congr, rw [← normalize_lcm a b] },
     erw [← normalize.map_mul, ← classical.some_spec (exists_gcd a b), normalize_idem] },

src/algebra/geom_sum.lean

@@ -301,7 +301,7 @@ have h₂ : x⁻¹ - 1 ≠ 0, from mt sub_eq_zero.1 h₁,
 have h₃ : x - 1 ≠ 0, from mt sub_eq_zero.1 hx1,
 have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x :=
   nat.rec_on n (by simp)
-  (λ n h, by rw [pow_succ, mul_inv_rev', ←mul_assoc, h, mul_assoc, mul_inv_cancel hx0, mul_assoc,
+  (λ n h, by rw [pow_succ, mul_inv_rev₀, ←mul_assoc, h, mul_assoc, mul_inv_cancel hx0, mul_assoc,
     inv_mul_cancel hx0]),
 begin
   rw [geom_sum_eq h₁, div_eq_iff_mul_eq h₂, ← mul_right_inj' h₃,

src/algebra/group/conj.lean

@@ -86,7 +86,7 @@ lemma conj_injective {x : α} : function.injective (λ (g : α), x * g * x⁻¹)
 
 end group
 
-@[simp] lemma is_conj_iff' [group_with_zero α] {a b : α} :
+@[simp] lemma is_conj_iff₀ [group_with_zero α] {a b : α} :
   is_conj a b ↔ ∃ c : α, c ≠ 0 ∧ c * a * c⁻¹ = b :=
 ⟨λ ⟨c, hc⟩, ⟨c, begin
     rw [← units.coe_inv', units.mul_inv_eq_iff_eq_mul],