refactor(*): rename ordered groups/monoids to ordered add_ groups/monoids (#2347)

In the perfectoid project we need ordered commutative monoids, and they are multiplicative. So the additive versions should be renamed to make some place.

Author: jcommelin

scripts/nolints.txt

@@ -3492,4 +3492,4 @@ apply_nolint uniform_space.separation_setoid doc_blame
 
 -- topology/uniform_space/uniform_embedding.lean
 apply_nolint uniform_embedding doc_blame
-apply_nolint uniform_inducing doc_blame
+apply_nolint uniform_inducing doc_blame

src/algebra/archimedean.lean

@@ -12,7 +12,7 @@ variables {α : Type*}
 
 open_locale add_monoid
 
-class archimedean (α) [ordered_comm_monoid α] : Prop :=
+class archimedean (α) [ordered_add_comm_monoid α] : Prop :=
 (arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)
 
 theorem exists_nat_gt [linear_ordered_semiring α] [archimedean α]

src/algebra/big_operators.lean

@@ -590,7 +590,7 @@ theorem dvd_sum [comm_semiring α] {a : α} {s : finset β} {f : β → α}
   (h : ∀ x ∈ s, a ∣ f x) : a ∣ s.sum f :=
 multiset.dvd_sum (λ y hy, by rcases multiset.mem_map.1 hy with ⟨x, hx, rfl⟩; exact h x hx)
 
-lemma le_sum_of_subadditive [add_comm_monoid α] [ordered_comm_monoid β]
+lemma le_sum_of_subadditive [add_comm_monoid α] [ordered_add_comm_monoid β]
   (f : α → β) (h_zero : f 0 = 0) (h_add : ∀x y, f (x + y) ≤ f x + f y) (s : finset γ) (g : γ → α) :
   f (s.sum g) ≤ s.sum (λc, f (g c)) :=
 begin
@@ -793,8 +793,8 @@ end
 
 end integral_domain
 
-section ordered_comm_monoid
-variables [ordered_comm_monoid β]
+section ordered_add_comm_monoid
+variables [ordered_add_comm_monoid β]
 
 lemma sum_le_sum : (∀x∈s, f x ≤ g x) → s.sum f ≤ s.sum g :=
 begin
@@ -839,10 +839,10 @@ have (singleton a).sum f ≤ s.sum f,
   (λ x e, (mem_singleton.1 e).symm ▸ h) (λ x h _, hf x h),
 by rwa sum_singleton at this
 
-end ordered_comm_monoid
+end ordered_add_comm_monoid
 
-section canonically_ordered_monoid
-variables [canonically_ordered_monoid β]
+section canonically_ordered_add_monoid
+variables [canonically_ordered_add_monoid β]
 
 lemma sum_le_sum_of_subset (h : s₁ ⊆ s₂) : s₁.sum f ≤ s₂.sum f :=
 sum_le_sum_of_subset_of_nonneg h $ assume x h₁ h₂, zero_le _
@@ -857,7 +857,7 @@ calc s₁.sum f = (s₁.filter (λx, f x = 0)).sum f + (s₁.filter (λx, f x 
       (sum_nonpos $ by simp only [mem_filter, and_imp]; exact λ _ _, le_of_eq)
       (sum_le_sum_of_subset $ by simpa only [subset_iff, mem_filter, and_imp])
 
-end canonically_ordered_monoid
+end canonically_ordered_add_monoid
 
 section ordered_cancel_comm_monoid
 
@@ -1067,7 +1067,7 @@ open finset
 open_locale classical
 
 /-- sum of finite numbers is still finite -/
-lemma sum_lt_top [ordered_comm_monoid β] {s : finset α} {f : α → with_top β} :
+lemma sum_lt_top [ordered_add_comm_monoid β] {s : finset α} {f : α → with_top β} :
   (∀a∈s, f a < ⊤) → s.sum f < ⊤ :=
 finset.induction_on s (by { intro h, rw sum_empty, exact coe_lt_top _ })
   (λa s ha ih h,
@@ -1078,7 +1078,7 @@ finset.induction_on s (by { intro h, rw sum_empty, exact coe_lt_top _ })
   end)
 
 /-- sum of finite numbers is still finite -/
-lemma sum_lt_top_iff [canonically_ordered_monoid β] {s : finset α} {f : α → with_top β} :
+lemma sum_lt_top_iff [canonically_ordered_add_monoid β] {s : finset α} {f : α → with_top β} :
   s.sum f < ⊤ ↔ (∀a∈s, f a < ⊤) :=
 iff.intro (λh a ha, lt_of_le_of_lt (single_le_sum (λa ha, zero_le _) ha) h) sum_lt_top
 

src/algebra/group_power.lean

@@ -472,7 +472,7 @@ end
 @[field_simps] theorem pow_ne_zero [domain R] {a : R} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 mt pow_eq_zero h
 
-theorem add_monoid.smul_nonneg [ordered_comm_monoid R] {a : R} (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ n • a
+theorem add_monoid.smul_nonneg [ordered_add_comm_monoid R] {a : R} (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ n • a
 | 0     := le_refl _
 | (n+1) := add_nonneg' H (add_monoid.smul_nonneg n)
 
@@ -484,7 +484,7 @@ lemma abs_neg_one_pow [decidable_linear_ordered_comm_ring R] (n : ℕ) : abs ((-
 by rw [←pow_abs, abs_neg, abs_one, one_pow]
 
 namespace add_monoid
-variable [ordered_comm_monoid A]
+variable [ordered_add_comm_monoid A]
 
 theorem smul_le_smul {a : A} {n m : ℕ} (ha : 0 ≤ a) (h : n ≤ m) : n • a ≤ m • a :=
 let ⟨k, hk⟩ := nat.le.dest h in

src/algebra/order_functions.lean

@@ -181,7 +181,7 @@ lemma min_mul_max [decidable_linear_order α] [comm_semigroup α] (n m : α) :
   min n m * max n m = n * m :=
 fn_min_mul_fn_max id n m
 
-section decidable_linear_ordered_comm_group
+section decidable_linear_ordered_add_comm_group
 variables [decidable_linear_ordered_add_comm_group α] {a b c : α}
 
 attribute [simp] abs_zero abs_neg
@@ -283,7 +283,7 @@ end
 lemma max_sub_min_eq_abs (a b : α) : max a b - min a b = abs (b - a) :=
 by { rw [abs_sub], exact max_sub_min_eq_abs' _ _ }
 
-end decidable_linear_ordered_comm_group
+end decidable_linear_ordered_add_comm_group
 
 section decidable_linear_ordered_semiring
 variables [decidable_linear_ordered_semiring α] {a b c d : α}

src/algebra/ordered_group.lean

@@ -18,7 +18,7 @@ set_option default_priority 100 -- see Note [default priority]
 /-- An ordered (additive) commutative monoid is a commutative monoid
   with a partial order such that addition is an order embedding, i.e.
   `a + b ≤ a + c ↔ b ≤ c`. These monoids are automatically cancellative. -/
-class ordered_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=
+class ordered_add_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=
 (add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
 (lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)
 
@@ -27,22 +27,22 @@ class ordered_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order
   which is to say, `a ≤ b` iff there exists `c` with `b = a + c`.
   This is satisfied by the natural numbers, for example, but not
   the integers or other ordered groups. -/
-class canonically_ordered_monoid (α : Type*) extends ordered_comm_monoid α, order_bot α :=
+class canonically_ordered_add_monoid (α : Type*) extends ordered_add_comm_monoid α, order_bot α :=
 (le_iff_exists_add : ∀a b:α, a ≤ b ↔ ∃c, b = a + c)
 
 end old_structure_cmd
 
-section ordered_comm_monoid
-variables [ordered_comm_monoid α] {a b c d : α}
+section ordered_add_comm_monoid
+variables [ordered_add_comm_monoid α] {a b c d : α}
 
 lemma add_le_add_left' (h : a ≤ b) : c + a ≤ c + b :=
-ordered_comm_monoid.add_le_add_left a b h c
+ordered_add_comm_monoid.add_le_add_left a b h c
 
 lemma add_le_add_right' (h : a ≤ b) : a + c ≤ b + c :=
 add_comm c a ▸ add_comm c b ▸ add_le_add_left' h
 
 lemma lt_of_add_lt_add_left' : a + b < a + c → b < c :=
-ordered_comm_monoid.lt_of_add_lt_add_left a b c
+ordered_add_comm_monoid.lt_of_add_lt_add_left a b c
 
 lemma add_le_add' (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
 le_trans (add_le_add_right' h₁) (add_le_add_left' h₂)
@@ -133,7 +133,7 @@ iff.intro
 lemma bit0_pos {a : α} (h : 0 < a) : 0 < bit0 a :=
 add_pos' h h
 
-end ordered_comm_monoid
+end ordered_add_comm_monoid
 
 namespace units
 
@@ -176,10 +176,10 @@ instance [decidable_linear_order α] :
  decidable_linear_order (with_zero α) := with_bot.decidable_linear_order
 
 /--
-If `0` is the least element in `α`, then `with_zero α` is an `ordered_comm_monoid`.
+If `0` is the least element in `α`, then `with_zero α` is an `ordered_add_comm_monoid`.
 -/
-def ordered_comm_monoid [ordered_comm_monoid α]
-  (zero_le : ∀ a : α, 0 ≤ a) : ordered_comm_monoid (with_zero α) :=
+def ordered_add_comm_monoid [ordered_add_comm_monoid α]
+  (zero_le : ∀ a : α, 0 ≤ a) : ordered_add_comm_monoid (with_zero α) :=
 begin
   suffices, refine {
     add_le_add_left := this,
@@ -236,7 +236,7 @@ instance [add_comm_monoid α] : add_comm_monoid (with_top α) :=
   ..@additive.add_comm_monoid _ $
     @with_zero.comm_monoid (multiplicative α) _ }
 
-instance [ordered_comm_monoid α] : ordered_comm_monoid (with_top α) :=
+instance [ordered_add_comm_monoid α] : ordered_add_comm_monoid (with_top α) :=
 begin
   suffices, refine {
     add_le_add_left := this,
@@ -260,22 +260,22 @@ begin
     exact ⟨_, rfl, add_le_add_left' h⟩, }
 end
 
-@[simp] lemma zero_lt_top [ordered_comm_monoid α] : (0 : with_top α) < ⊤ :=
+@[simp] lemma zero_lt_top [ordered_add_comm_monoid α] : (0 : with_top α) < ⊤ :=
 coe_lt_top 0
 
-@[simp] lemma zero_lt_coe [ordered_comm_monoid α] (a : α) : (0 : with_top α) < a ↔ 0 < a :=
+@[simp] lemma zero_lt_coe [ordered_add_comm_monoid α] (a : α) : (0 : with_top α) < a ↔ 0 < a :=
 coe_lt_coe
 
-@[simp] lemma add_top [ordered_comm_monoid α] : ∀{a : with_top α}, a + ⊤ = ⊤
+@[simp] lemma add_top [ordered_add_comm_monoid α] : ∀{a : with_top α}, a + ⊤ = ⊤
 | none := rfl
 | (some a) := rfl
 
-@[simp] lemma top_add [ordered_comm_monoid α] {a : with_top α} : ⊤ + a = ⊤ := rfl
+@[simp] lemma top_add [ordered_add_comm_monoid α] {a : with_top α} : ⊤ + a = ⊤ := rfl
 
-lemma add_eq_top [ordered_comm_monoid α] (a b : with_top α) : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
+lemma add_eq_top [ordered_add_comm_monoid α] (a b : with_top α) : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
 by cases a; cases b; simp [none_eq_top, some_eq_coe, coe_add.symm]
 
-lemma add_lt_top [ordered_comm_monoid α] (a b : with_top α) : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
+lemma add_lt_top [ordered_add_comm_monoid α] (a b : with_top α) : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
 begin
   apply not_iff_not.1,
   simp [lt_top_iff_ne_top, add_eq_top],
@@ -284,21 +284,21 @@ begin
   apply classical.dec _,
 end
 
-instance [canonically_ordered_monoid α] : canonically_ordered_monoid (with_top α) :=
+instance [canonically_ordered_add_monoid α] : canonically_ordered_add_monoid (with_top α) :=
 { le_iff_exists_add := assume a b,
   match a, b with
   | a, none     := show a ≤ ⊤ ↔ ∃c, ⊤ = a + c, by simp; refine ⟨⊤, _⟩; cases a; refl
   | (some a), (some b) := show (a:with_top α) ≤ ↑b ↔ ∃c:with_top α, ↑b = ↑a + c,
     begin
-      simp [canonically_ordered_monoid.le_iff_exists_add, -add_comm],
+      simp [canonically_ordered_add_monoid.le_iff_exists_add, -add_comm],
       split,
       { rintro ⟨c, rfl⟩, refine ⟨c, _⟩, simp [coe_add] },
       { exact assume h, match b, h with _, ⟨some c, rfl⟩ := ⟨_, rfl⟩ end }
     end
   | none, some b := show (⊤ : with_top α) ≤ b ↔ ∃c:with_top α, ↑b = ⊤ + c, by simp
   end,
   .. with_top.order_bot,
-  .. with_top.ordered_comm_monoid }
+  .. with_top.ordered_add_comm_monoid }
 
 end with_top
 
@@ -309,7 +309,7 @@ instance [add_comm_semigroup α] : add_comm_semigroup (with_bot α) := with_top.
 instance [add_monoid α] : add_monoid (with_bot α) := with_top.add_monoid
 instance [add_comm_monoid α] : add_comm_monoid (with_bot α) :=  with_top.add_comm_monoid
 
-instance [ordered_comm_monoid α] : ordered_comm_monoid (with_bot α) :=
+instance [ordered_add_comm_monoid α] : ordered_add_comm_monoid (with_bot α) :=
 begin
   suffices, refine {
     add_le_add_left := this,
@@ -337,21 +337,21 @@ end
 
 @[simp] lemma coe_add [add_semigroup α] (a b : α) : ((a + b : α) : with_bot α) = a + b := rfl
 
-@[simp] lemma bot_add [ordered_comm_monoid α] (a : with_bot α) : ⊥ + a = ⊥ := rfl
+@[simp] lemma bot_add [ordered_add_comm_monoid α] (a : with_bot α) : ⊥ + a = ⊥ := rfl
 
-@[simp] lemma add_bot [ordered_comm_monoid α] (a : with_bot α) : a + ⊥ = ⊥ := by cases a; refl
+@[simp] lemma add_bot [ordered_add_comm_monoid α] (a : with_bot α) : a + ⊥ = ⊥ := by cases a; refl
 
 instance has_one [has_one α] : has_one (with_bot α) := ⟨(1 : α)⟩
 
 @[simp] lemma coe_one [has_one α] : ((1 : α) : with_bot α) = 1 := rfl
 
 end with_bot
 
-section canonically_ordered_monoid
-variables [canonically_ordered_monoid α] {a b c d : α}
+section canonically_ordered_add_monoid
+variables [canonically_ordered_add_monoid α] {a b c d : α}
 
 lemma le_iff_exists_add : a ≤ b ↔ ∃c, b = a + c :=
-canonically_ordered_monoid.le_iff_exists_add a b
+canonically_ordered_add_monoid.le_iff_exists_add a b
 
 @[simp] lemma zero_le (a : α) : 0 ≤ a := le_iff_exists_add.mpr ⟨a, by simp⟩
 
@@ -377,8 +377,8 @@ lemma le_add_right (h : a ≤ b) : a ≤ b + c :=
 calc a = a + 0 : by simp
   ... ≤ b + c : add_le_add' h (zero_le _)
 
-instance with_zero.canonically_ordered_monoid :
-  canonically_ordered_monoid (with_zero α) :=
+instance with_zero.canonically_ordered_add_monoid :
+  canonically_ordered_add_monoid (with_zero α) :=
 { le_iff_exists_add := λ a b, begin
     cases a with a,
     { exact iff_of_true bot_le ⟨b, (zero_add b).symm⟩ },
@@ -395,13 +395,13 @@ instance with_zero.canonically_ordered_monoid :
   end,
   bot    := 0,
   bot_le := assume a a' h, option.no_confusion h,
-  .. with_zero.ordered_comm_monoid zero_le }
+  .. with_zero.ordered_add_comm_monoid zero_le }
 
-end canonically_ordered_monoid
+end canonically_ordered_add_monoid
 
 @[priority 100] -- see Note [lower instance priority]
 instance ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid
-  [H : ordered_cancel_add_comm_monoid α] : ordered_comm_monoid α :=
+  [H : ordered_cancel_add_comm_monoid α] : ordered_add_comm_monoid α :=
 { lt_of_add_lt_add_left := @lt_of_add_lt_add_left _ _, ..H }
 
 section ordered_cancel_comm_monoid
@@ -471,13 +471,13 @@ by simpa [add_comm] using @with_top.add_lt_add_iff_left _ _ a b c
 
 end ordered_cancel_comm_monoid
 
-section ordered_comm_group
+section ordered_add_comm_group
 
 /--
-The `add_lt_add_left` field of `ordered_comm_group` is redundant, but it is in core so
+The `add_lt_add_left` field of `ordered_add_comm_group` is redundant, but it is in core so
 we can't remove it for now. This alternative constructor is the best we can do.
 -/
-def ordered_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α]
+def ordered_add_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α]
   (add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) :
   ordered_add_comm_group α :=
 { add_le_add_left := add_le_add_left,
@@ -655,7 +655,7 @@ sub_le_iff_le_add'.trans (le_add_iff_nonneg_left _)
 lemma sub_lt_self_iff (a : α) {b : α} : a - b < a ↔ 0 < b :=
 sub_lt_iff_lt_add'.trans (lt_add_iff_pos_left _)
 
-end ordered_comm_group
+end ordered_add_comm_group
 
 namespace decidable_linear_ordered_add_comm_group
 variables [s : decidable_linear_ordered_add_comm_group α]
@@ -678,7 +678,7 @@ section prio
 set_option default_priority 100 -- see Note [default priority]
 /-- This is not so much a new structure as a construction mechanism
   for ordered groups, by specifying only the "positive cone" of the group. -/
-class nonneg_comm_group (α : Type*) extends add_comm_group α :=
+class nonneg_add_comm_group (α : Type*) extends add_comm_group α :=
 (nonneg : α → Prop)
 (pos : α → Prop := λ a, nonneg a ∧ ¬ nonneg (neg a))
 (pos_iff : ∀ a, pos a ↔ nonneg a ∧ ¬ nonneg (-a) . order_laws_tac)
@@ -687,8 +687,8 @@ class nonneg_comm_group (α : Type*) extends add_comm_group α :=
 (nonneg_antisymm : ∀ {a}, nonneg a → nonneg (-a) → a = 0)
 end prio
 
-namespace nonneg_comm_group
-variable [s : nonneg_comm_group α]
+namespace nonneg_add_comm_group
+variable [s : nonneg_add_comm_group α]
 include s
 
 @[reducible, priority 100] -- see Note [lower instance priority]
@@ -724,7 +724,7 @@ theorem nonneg_total_iff :
  λ h a, by rw [nonneg_def, nonneg_def, neg_nonneg]; apply h⟩
 
 /--
-A `nonneg_comm_group` is a `decidable_linear_ordered_add_comm_group`
+A `nonneg_add_comm_group` is a `decidable_linear_ordered_add_comm_group`
 if `nonneg` is total and decidable.
 -/
 def to_decidable_linear_ordered_add_comm_group
@@ -740,13 +740,13 @@ def to_decidable_linear_ordered_add_comm_group
   le_total := nonneg_total_iff.1 nonneg_total,
   decidable_le := by apply_instance,
   decidable_lt := by apply_instance,
-  ..@nonneg_comm_group.to_ordered_add_comm_group _ s }
+  ..@nonneg_add_comm_group.to_ordered_add_comm_group _ s }
 
-end nonneg_comm_group
+end nonneg_add_comm_group
 
 namespace order_dual
 
-instance [ordered_comm_monoid α] : ordered_comm_monoid (order_dual α) :=
+instance [ordered_add_comm_monoid α] : ordered_add_comm_monoid (order_dual α) :=
 { add_le_add_left := λ a b h c, @add_le_add_left' α _ b a c h,
   lt_of_add_lt_add_left := λ a b c h, @lt_of_add_lt_add_left' α _ a c b h,
   ..order_dual.partial_order α,
@@ -756,11 +756,11 @@ instance [ordered_cancel_add_comm_monoid α] : ordered_cancel_add_comm_monoid (o
 { le_of_add_le_add_left := λ a b c : α, le_of_add_le_add_left,
   add_left_cancel := @add_left_cancel α _,
   add_right_cancel := @add_right_cancel α _,
-  ..order_dual.ordered_comm_monoid }
+  ..order_dual.ordered_add_comm_monoid }
 
 instance [ordered_add_comm_group α] : ordered_add_comm_group (order_dual α) :=
 { add_left_neg := λ a : α, add_left_neg a,
-  ..order_dual.ordered_comm_monoid,
+  ..order_dual.ordered_add_comm_monoid,
   ..show add_comm_group α, by apply_instance }
 
 end order_dual