chore(algebra/group_with_zero/defs: Rename `comm_cancel_monoid_with_z…

…ero` to `cancel_comm_monoid_with_zero` (#10669)

We currently have `cancel_comm_monoid` but `comm_cancel_monoid_with_zero`. This renames the latter to follow the former.

Replaced `comm_cancel_` by `cancel_comm_` everywhere.

src/algebra/associated.lean

@@ -28,14 +28,14 @@ is_unit_iff_dvd_one.2 $ xy.trans $ is_unit_iff_dvd_one.1 hu
 lemma is_unit_of_dvd_one [comm_monoid α] : ∀a ∣ 1, is_unit (a:α)
 | a ⟨b, eq⟩ := ⟨units.mk_of_mul_eq_one a b eq.symm, rfl⟩
 
-lemma dvd_and_not_dvd_iff [comm_cancel_monoid_with_zero α] {x y : α} :
+lemma dvd_and_not_dvd_iff [cancel_comm_monoid_with_zero α] {x y : α} :
   x ∣ y ∧ ¬y ∣ x ↔ dvd_not_unit 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]⟩)⟩⟩
 
-lemma pow_dvd_pow_iff [comm_cancel_monoid_with_zero α]
+lemma pow_dvd_pow_iff [cancel_comm_monoid_with_zero α]
   {x : α} {n m : ℕ} (h0 : x ≠ 0) (h1 : ¬ is_unit x) :
   x ^ n ∣ x ^ m ↔ n ≤ m :=
 begin
@@ -117,7 +117,7 @@ end prime
 
 end prime
 
-lemma prime.left_dvd_or_dvd_right_of_dvd_mul [comm_cancel_monoid_with_zero α] {p : α}
+lemma prime.left_dvd_or_dvd_right_of_dvd_mul [cancel_comm_monoid_with_zero α] {p : α}
   (hp : prime p) {a b : α} : a ∣ p * b → p ∣ a ∨ a ∣ b :=
 begin
   rintro ⟨c, hc⟩,
@@ -176,7 +176,7 @@ begin
   exact H _ o.1 _ o.2 h.symm
 end
 
-protected lemma prime.irreducible [comm_cancel_monoid_with_zero α] {p : α} (hp : prime p) :
+protected lemma prime.irreducible [cancel_comm_monoid_with_zero α] {p : α} (hp : prime p) :
   irreducible p :=
 ⟨hp.not_unit, λ a b hab,
   (show a * b ∣ a ∨ a * b ∣ b, from hab ▸ hp.dvd_or_dvd (hab ▸ dvd_rfl)).elim
@@ -187,7 +187,7 @@ protected lemma prime.irreducible [comm_cancel_monoid_with_zero α] {p : α} (hp
       ⟨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 α]
+lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul [cancel_comm_monoid_with_zero α]
   {p : α} (hp : prime p) {a b : α} {k l : ℕ} :
   p ^ k ∣ a → p ^ l ∣ b → p ^ ((k + l) + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b :=
 λ ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩,
@@ -318,7 +318,7 @@ end
 theorem dvd_dvd_iff_associated [cancel_monoid_with_zero α] {a b : α} : a ∣ b ∧ b ∣ a ↔ a ~ᵤ b :=
 ⟨λ ⟨h1, h2⟩, associated_of_dvd_dvd h1 h2, associated.dvd_dvd⟩
 
-lemma exists_associated_mem_of_dvd_prod [comm_cancel_monoid_with_zero α] {p : α}
+lemma exists_associated_mem_of_dvd_prod [cancel_comm_monoid_with_zero α] {p : α}
   (hp : prime p) {s : multiset α} : (∀ r ∈ s, prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
 multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
   (λ a s ih hs hps, begin
@@ -362,11 +362,11 @@ lemma irreducible.dvd_irreducible_iff_associated [cancel_monoid_with_zero α]
   p ∣ q ↔ associated p q :=
 ⟨irreducible.associated_of_dvd pp qp, associated.dvd⟩
 
-lemma prime.associated_of_dvd [comm_cancel_monoid_with_zero α] {p q : α}
+lemma prime.associated_of_dvd [cancel_comm_monoid_with_zero α] {p q : α}
   (p_prime : prime p) (q_prime : prime q) (dvd : p ∣ q) : associated p q :=
 p_prime.irreducible.associated_of_dvd q_prime.irreducible dvd
 
-theorem prime.dvd_prime_iff_associated [comm_cancel_monoid_with_zero α]
+theorem prime.dvd_prime_iff_associated [cancel_comm_monoid_with_zero α]
   {p q : α} (pp : prime p) (qp : prime q) :
   p ∣ q ↔ associated p q :=
 pp.irreducible.dvd_irreducible_iff_associated qp.irreducible
@@ -393,7 +393,7 @@ protected lemma associated.irreducible_iff [monoid α] {p q : α} (h : p ~ᵤ q)
   irreducible p ↔ irreducible q :=
 ⟨h.irreducible, h.symm.irreducible⟩
 
-lemma associated.of_mul_left [comm_cancel_monoid_with_zero α] {a b c d : α}
+lemma associated.of_mul_left [cancel_comm_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
@@ -402,7 +402,7 @@ let ⟨u, hu⟩ := h in let ⟨v, hv⟩ := associated.symm h₁ in
     simp [hv.symm, mul_assoc, mul_comm, mul_left_comm]
   end⟩
 
-lemma associated.of_mul_right [comm_cancel_monoid_with_zero α] {a b c d : α} :
+lemma associated.of_mul_right [cancel_comm_monoid_with_zero α] {a b c d : α} :
   a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c :=
 by rw [mul_comm a, mul_comm c]; exact associated.of_mul_left
 
@@ -715,8 +715,8 @@ end
 
 end comm_monoid_with_zero
 
-section comm_cancel_monoid_with_zero
-variable [comm_cancel_monoid_with_zero α]
+section cancel_comm_monoid_with_zero
+variable [cancel_comm_monoid_with_zero α]
 
 instance : partial_order (associates α) :=
 { le_antisymm := λ a' b', quotient.induction_on₂ a' b' (λ a b hab hba,
@@ -770,7 +770,7 @@ match h m d dvd_rfl with
   or.inl $ bot_unique $ associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
 end
 
-instance : comm_cancel_monoid_with_zero (associates α) :=
+instance : cancel_comm_monoid_with_zero (associates α) :=
 { mul_left_cancel_of_ne_zero := eq_of_mul_eq_mul_left,
   mul_right_cancel_of_ne_zero := eq_of_mul_eq_mul_right,
   .. (infer_instance : comm_monoid_with_zero (associates α)) }
@@ -779,13 +779,13 @@ theorem dvd_not_unit_iff_lt {a b : associates α} :
   dvd_not_unit a b ↔ a < b :=
 dvd_and_not_dvd_iff.symm
 
-end comm_cancel_monoid_with_zero
+end cancel_comm_monoid_with_zero
 
 end associates
 
 namespace multiset
 
-lemma prod_ne_zero_of_prime [comm_cancel_monoid_with_zero α] [nontrivial α]
+lemma prod_ne_zero_of_prime [cancel_comm_monoid_with_zero α] [nontrivial α]
  (s : multiset α) (h : ∀ x ∈ s, prime x) : s.prod ≠ 0 :=
 multiset.prod_ne_zero (λ h0, prime.ne_zero (h 0 h0) rfl)
 

src/algebra/divisibility.lean

@@ -160,7 +160,7 @@ exists_congr $ λ d, by rw [mul_assoc, mul_right_inj' ha]
 
 /-- Given two elements `a`, `b` of a commutative `cancel_monoid_with_zero` and a nonzero
   element `c`, `a*c` divides `b*c` iff `a` divides `b`. -/
-theorem mul_dvd_mul_iff_right [comm_cancel_monoid_with_zero α] {a b c : α} (hc : c ≠ 0) :
+theorem mul_dvd_mul_iff_right [cancel_comm_monoid_with_zero α] {a b c : α} (hc : c ≠ 0) :
   a * c ∣ b * c ↔ a ∣ b :=
 exists_congr $ λ d, by rw [mul_right_comm, mul_left_inj' hc]
 

src/algebra/gcd_monoid/basic.lean

@@ -10,7 +10,7 @@ import algebra.group_power.lemmas
 /-!
 # Monoids with normalization functions, `gcd`, and `lcm`
 
-This file defines extra structures on `comm_cancel_monoid_with_zero`s, including `is_domain`s.
+This file defines extra structures on `cancel_comm_monoid_with_zero`s, including `is_domain`s.
 
 ## Main Definitions
 
@@ -69,7 +69,7 @@ variables {α : Type*}
 /-- Normalization monoid: multiplying with `norm_unit` gives a normal form for associated
 elements. -/
 @[protect_proj] class normalization_monoid (α : Type*)
-  [comm_cancel_monoid_with_zero α] :=
+  [cancel_comm_monoid_with_zero α] :=
 (norm_unit : α → units α)
 (norm_unit_zero      : norm_unit 0 = 1)
 (norm_unit_mul       : ∀{a b}, a ≠ 0 → b ≠ 0 → norm_unit (a * b) = norm_unit a * norm_unit b)
@@ -80,7 +80,7 @@ export normalization_monoid (norm_unit norm_unit_zero norm_unit_mul norm_unit_co
 attribute [simp] norm_unit_coe_units norm_unit_zero norm_unit_mul
 
 section normalization_monoid
-variables [comm_cancel_monoid_with_zero α] [normalization_monoid α]
+variables [cancel_comm_monoid_with_zero α] [normalization_monoid α]
 
 @[simp] theorem norm_unit_one : norm_unit (1:α) = 1 :=
 norm_unit_coe_units 1
@@ -162,7 +162,7 @@ units.mul_right_dvd
 end normalization_monoid
 
 namespace associates
-variables [comm_cancel_monoid_with_zero α] [normalization_monoid α]
+variables [cancel_comm_monoid_with_zero α] [normalization_monoid α]
 
 local attribute [instance] associated.setoid
 
@@ -202,11 +202,11 @@ function.left_inverse.injective mk_out
 
 end associates
 
-/-- GCD monoid: a `comm_cancel_monoid_with_zero` with `gcd` (greatest common divisor) and
+/-- GCD monoid: a `cancel_comm_monoid_with_zero` with `gcd` (greatest common divisor) and
 `lcm` (least common multiple) operations, determined up to a unit. The type class focuses on `gcd`
 and we derive the corresponding `lcm` facts from `gcd`.
 -/
-@[protect_proj] class gcd_monoid (α : Type*) [comm_cancel_monoid_with_zero α] :=
+@[protect_proj] class gcd_monoid (α : Type*) [cancel_comm_monoid_with_zero α] :=
 (gcd : α → α → α)
 (lcm : α → α → α)
 (gcd_dvd_left   : ∀a b, gcd a b ∣ a)
@@ -216,13 +216,13 @@ and we derive the corresponding `lcm` facts from `gcd`.
 (lcm_zero_left  : ∀a, lcm 0 a = 0)
 (lcm_zero_right : ∀a, lcm a 0 = 0)
 
-/-- Normalized GCD monoid: a `comm_cancel_monoid_with_zero` with normalization and `gcd`
+/-- Normalized GCD monoid: a `cancel_comm_monoid_with_zero` with normalization and `gcd`
 (greatest common divisor) and `lcm` (least common multiple) operations. In this setting `gcd` and
 `lcm` form a bounded lattice on the associated elements where `gcd` is the infimum, `lcm` is the
 supremum, `1` is bottom, and `0` is top. The type class focuses on `gcd` and we derive the
 corresponding `lcm` facts from `gcd`.
 -/
-class normalized_gcd_monoid (α : Type*) [comm_cancel_monoid_with_zero α]
+class normalized_gcd_monoid (α : Type*) [cancel_comm_monoid_with_zero α]
   extends normalization_monoid α, gcd_monoid α :=
 (normalize_gcd : ∀a b, normalize (gcd a b) = gcd a b)
 (normalize_lcm : ∀a b, normalize (lcm a b) = lcm a b)
@@ -233,7 +233,7 @@ export gcd_monoid (gcd lcm gcd_dvd_left gcd_dvd_right dvd_gcd  lcm_zero_left lcm
 attribute [simp] lcm_zero_left lcm_zero_right
 
 section gcd_monoid
-variables [comm_cancel_monoid_with_zero α]
+variables [cancel_comm_monoid_with_zero α]
 
 @[simp] theorem normalize_gcd [normalized_gcd_monoid α] : ∀a b:α, normalize (gcd a b) = gcd a b :=
 normalized_gcd_monoid.normalize_gcd
@@ -700,7 +700,7 @@ end gcd_monoid
 
 section unique_unit
 
-variables [comm_cancel_monoid_with_zero α] [unique (units α)]
+variables [cancel_comm_monoid_with_zero α] [unique (units α)]
 
 @[priority 100] -- see Note [lower instance priority]
 instance normalization_monoid_of_unique_units : normalization_monoid α :=
@@ -754,7 +754,7 @@ noncomputable theory
 
 open associates
 
-variables [comm_cancel_monoid_with_zero α]
+variables [cancel_comm_monoid_with_zero α]
 
 private lemma map_mk_unit_aux [decidable_eq α] {f : associates α →* α}
   (hinv : function.right_inverse f associates.mk) (a : α) :

src/algebra/gcd_monoid/finset.lean

@@ -31,7 +31,7 @@ variables {α β γ : Type*}
 namespace finset
 open multiset
 
-variables [comm_cancel_monoid_with_zero α] [normalized_gcd_monoid α]
+variables [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α]
 
 /-! ### lcm -/
 section lcm

src/algebra/gcd_monoid/multiset.lean

@@ -24,7 +24,7 @@ multiset, gcd
 -/
 
 namespace multiset
-variables {α : Type*} [comm_cancel_monoid_with_zero α] [normalized_gcd_monoid α]
+variables {α : Type*} [cancel_comm_monoid_with_zero α] [normalized_gcd_monoid α]
 
 /-! ### lcm -/
 section lcm

src/algebra/group_with_zero/basic.lean

@@ -470,22 +470,22 @@ classical.by_contradiction $ λ ha, h₁ $ mul_right_cancel₀ ha $ h₂.symm 
 
 end cancel_monoid_with_zero
 
-section comm_cancel_monoid_with_zero
+section cancel_comm_monoid_with_zero
 
-variables [comm_cancel_monoid_with_zero M₀] {a b c : M₀}
+variables [cancel_comm_monoid_with_zero M₀] {a b c : M₀}
 
-/-- Pullback a `comm_cancel_monoid_with_zero` class along an injective function.
+/-- Pullback a `cancel_comm_monoid_with_zero` class along an injective function.
 See note [reducible non-instances]. -/
 @[reducible]
-protected def function.injective.comm_cancel_monoid_with_zero
+protected def function.injective.cancel_comm_monoid_with_zero
   [has_zero M₀'] [has_mul M₀'] [has_one M₀']
   (f : M₀' → M₀) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
   (mul : ∀ x y, f (x * y) = f x * f y) :
-  comm_cancel_monoid_with_zero M₀' :=
+  cancel_comm_monoid_with_zero M₀' :=
 { .. hf.comm_monoid_with_zero f zero one mul,
   .. hf.cancel_monoid_with_zero f zero one mul }
 
-end comm_cancel_monoid_with_zero
+end cancel_comm_monoid_with_zero
 
 section group_with_zero
 variables [group_with_zero G₀] {a b c g h x : G₀}
@@ -931,7 +931,7 @@ section comm_group_with_zero -- comm
 variables [comm_group_with_zero G₀] {a b c : G₀}
 
 @[priority 10] -- see Note [lower instance priority]
-instance comm_group_with_zero.comm_cancel_monoid_with_zero : comm_cancel_monoid_with_zero G₀ :=
+instance comm_group_with_zero.cancel_comm_monoid_with_zero : cancel_comm_monoid_with_zero G₀ :=
 { ..group_with_zero.cancel_monoid_with_zero, ..comm_group_with_zero.to_comm_monoid_with_zero G₀ }
 
 /-- Pullback a `comm_group_with_zero` class along an injective function.

src/algebra/group_with_zero/defs.lean

@@ -101,10 +101,10 @@ element, and `0` is left and right absorbing. -/
 @[protect_proj]
 class comm_monoid_with_zero (M₀ : Type*) extends comm_monoid M₀, monoid_with_zero M₀.
 
-/-- A type `M` is a `comm_cancel_monoid_with_zero` if it is a commutative monoid with zero element,
+/-- A type `M` is a `cancel_comm_monoid_with_zero` if it is a commutative monoid with zero element,
  `0` is left and right absorbing,
   and left/right multiplication by a non-zero element is injective. -/
-@[protect_proj] class comm_cancel_monoid_with_zero (M₀ : Type*) extends
+@[protect_proj] class cancel_comm_monoid_with_zero (M₀ : Type*) extends
   comm_monoid_with_zero M₀, cancel_monoid_with_zero M₀.
 
 /-- A type `G₀` is a “group with zero” if it is a monoid with zero element (distinct from `1`)

src/algebra/punit_instances.lean

@@ -44,7 +44,7 @@ by refine
   .. };
 intros; exact subsingleton.elim _ _
 
-instance : comm_cancel_monoid_with_zero punit :=
+instance : cancel_comm_monoid_with_zero punit :=
 by refine
 { .. punit.comm_ring,
   .. };

src/algebra/ring/basic.lean

@@ -1022,7 +1022,7 @@ section comm_ring
 variables [comm_ring α] [is_domain α]
 
 @[priority 100] -- see Note [lower instance priority]
-instance is_domain.to_comm_cancel_monoid_with_zero : comm_cancel_monoid_with_zero α :=
+instance is_domain.to_cancel_comm_monoid_with_zero : cancel_comm_monoid_with_zero α :=
 { ..comm_semiring.to_comm_monoid_with_zero, ..is_domain.to_cancel_monoid_with_zero }
 
 lemma mul_self_eq_mul_self_iff {a b : α} : a * a = b * b ↔ a = b ∨ a = -b :=

src/algebra/squarefree.lean

@@ -61,7 +61,7 @@ begin
 end
 
 @[simp]
-lemma prime.squarefree [comm_cancel_monoid_with_zero R] {x : R} (h : prime x) :
+lemma prime.squarefree [cancel_comm_monoid_with_zero R] {x : R} (h : prime x) :
   squarefree x :=
 h.irreducible.squarefree
 
@@ -86,7 +86,7 @@ end
 end multiplicity
 
 namespace unique_factorization_monoid
-variables [comm_cancel_monoid_with_zero R] [nontrivial R] [unique_factorization_monoid R]
+variables [cancel_comm_monoid_with_zero R] [nontrivial R] [unique_factorization_monoid R]
 variables [normalization_monoid R]
 
 lemma squarefree_iff_nodup_normalized_factors [decidable_eq R] {x : R} (x0 : x ≠ 0) :

src/data/nat/basic.lean

@@ -122,7 +122,7 @@ rfl
 theorem nat.eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : 0 < m) (H : n * m = k * m) : n = k :=
 by rw [mul_comm n m, mul_comm k m] at H; exact nat.eq_of_mul_eq_mul_left Hm H
 
-instance nat.comm_cancel_monoid_with_zero : comm_cancel_monoid_with_zero ℕ :=
+instance nat.cancel_comm_monoid_with_zero : cancel_comm_monoid_with_zero ℕ :=
 { mul_left_cancel_of_ne_zero :=
     λ _ _ _ h1 h2, nat.eq_of_mul_eq_mul_left (nat.pos_of_ne_zero h1) h2,
   mul_right_cancel_of_ne_zero :=

src/ring_theory/dedekind_domain.lean

@@ -275,7 +275,7 @@ A Dedekind domain is an integral domain such that every fractional ideal has an
 This is equivalent to `is_dedekind_domain`.
 In particular we provide a `fractional_ideal.comm_group_with_zero` instance,
 assuming `is_dedekind_domain A`, which implies `is_dedekind_domain_inv`. For **integral** ideals,
-`is_dedekind_domain`(`_inv`) implies only `ideal.comm_cancel_monoid_with_zero`.
+`is_dedekind_domain`(`_inv`) implies only `ideal.cancel_comm_monoid_with_zero`.
 -/
 def is_dedekind_domain_inv : Prop :=
 ∀ I ≠ (⊥ : fractional_ideal A⁰ (fraction_ring A)), I * I⁻¹ = 1
@@ -666,9 +666,9 @@ noncomputable instance fractional_ideal.comm_group_with_zero :
   mul_inv_cancel := λ I, fractional_ideal.mul_inv_cancel,
   .. fractional_ideal.comm_semiring }
 
-noncomputable instance ideal.comm_cancel_monoid_with_zero :
-  comm_cancel_monoid_with_zero (ideal A) :=
-function.injective.comm_cancel_monoid_with_zero (coe_ideal_hom A⁰ (fraction_ring A))
+noncomputable instance ideal.cancel_comm_monoid_with_zero :
+  cancel_comm_monoid_with_zero (ideal A) :=
+function.injective.cancel_comm_monoid_with_zero (coe_ideal_hom A⁰ (fraction_ring A))
   coe_ideal_injective (ring_hom.map_zero _) (ring_hom.map_one _) (ring_hom.map_mul _)
 
 /-- For ideals in a Dedekind domain, to divide is to contain. -/

src/ring_theory/multiplicity.lean

@@ -298,9 +298,9 @@ end
 
 end comm_ring
 
-section comm_cancel_monoid_with_zero
+section cancel_comm_monoid_with_zero
 
-variables [comm_cancel_monoid_with_zero α]
+variables [cancel_comm_monoid_with_zero α]
 
 lemma finite_mul_aux {p : α} (hp : prime p) : ∀ {n m : ℕ} {a b : α},
   ¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b
@@ -433,7 +433,7 @@ lemma multiplicity_pow_self_of_prime {p : α} (hp : prime p) (n : ℕ) :
 multiplicity_pow_self hp.ne_zero hp.not_unit n
 
 
-end comm_cancel_monoid_with_zero
+end cancel_comm_monoid_with_zero
 
 section valuation