chore: Generalise monotonicity of multiplication lemmas to semirings (#…

…9369)

Many lemmas about `BlahOrderedRing α` did not mention negation. I could generalise almost all those lemmas to `BlahOrderedSemiring α` + `ExistsAddOfLE α` except for a series of five lemmas (left a TODO about them).

Now those lemmas apply to things like the naturals. This is not very useful on its own, because those lemmas are trivially true on canonically ordered semirings (they are about multiplication by negative elements, of which there are none, or nonnegativity of squares, but we already know everything is nonnegative), except that I will soon add more complicated inequalities that are based on those, and it would be a shame having to write two versions of each: one for ordered rings, one for canonically ordered semirings.

A similar refactor could be made for scalar multiplication, but this PR is big enough already.

From LeanAPAP

Mathlib.lean

@@ -205,6 +205,7 @@ import Mathlib.Algebra.Group.WithOne.Defs
 import Mathlib.Algebra.Group.WithOne.Units
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.GroupPower.CovariantClass
+import Mathlib.Algebra.GroupPower.Hom
 import Mathlib.Algebra.GroupPower.Identities
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.GroupPower.Lemmas

Mathlib/Algebra/Divisibility/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
 Neil Strickland, Aaron Anderson
 -/
-import Mathlib.Algebra.Group.Basic
+import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.Group.Hom.Defs
 
 #align_import algebra.divisibility.basic from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
@@ -115,8 +115,7 @@ end map_dvd
 end Semigroup
 
 section Monoid
-
-variable [Monoid α] {a b : α}
+variable [Monoid α] {a b : α} {m n : ℕ}
 
 @[refl, simp]
 theorem dvd_refl (a : α) : a ∣ a :=
@@ -139,6 +138,20 @@ theorem dvd_of_eq (h : a = b) : a ∣ b := by rw [h]
 alias Eq.dvd := dvd_of_eq
 #align eq.dvd Eq.dvd
 
+lemma pow_dvd_pow (a : α) (h : m ≤ n) : a ^ m ∣ a ^ n :=
+  ⟨a ^ (n - m), by rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]⟩
+#align pow_dvd_pow pow_dvd_pow
+
+lemma dvd_pow (hab : a ∣ b) : ∀ {n : ℕ} (_ : n ≠ 0), a ∣ b ^ n
+  | 0,     hn => (hn rfl).elim
+  | n + 1, _  => by rw [pow_succ]; exact hab.mul_right _
+#align dvd_pow dvd_pow
+
+alias Dvd.dvd.pow := dvd_pow
+
+lemma dvd_pow_self (a : α) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n := dvd_rfl.pow hn
+#align dvd_pow_self dvd_pow_self
+
 end Monoid
 
 section CommSemigroup

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yury Kudryashov
 -/
 import Mathlib.Data.List.BigOperators.Basic
+import Mathlib.GroupTheory.GroupAction.Defs
 
 #align_import algebra.free_monoid.basic from "leanprover-community/mathlib"@"657df4339ae6ceada048c8a2980fb10e393143ec"
 

Mathlib/Algebra/GroupPower/Basic.lean

@@ -3,9 +3,9 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
-import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Commute.Units
-import Mathlib.Algebra.Group.TypeTags
+import Mathlib.Algebra.GroupWithZero.Defs
+import Mathlib.Tactic.Convert
 
 #align_import algebra.group_power.basic from "leanprover-community/mathlib"@"9b2660e1b25419042c8da10bf411aa3c67f14383"
 
@@ -230,19 +230,6 @@ theorem pow_mul_pow_eq_one {a b : M} (n : ℕ) (h : a * b = 1) : a ^ n * b ^ n =
 #align pow_mul_pow_eq_one pow_mul_pow_eq_one
 #align nsmul_add_nsmul_eq_zero nsmul_add_nsmul_eq_zero
 
-theorem dvd_pow {x y : M} (hxy : x ∣ y) : ∀ {n : ℕ} (_ : n ≠ 0), x ∣ y ^ n
-  | 0,     hn => (hn rfl).elim
-  | n + 1, _  => by
-    rw [pow_succ]
-    exact hxy.mul_right _
-#align dvd_pow dvd_pow
-
-alias Dvd.dvd.pow := dvd_pow
-
-theorem dvd_pow_self (a : M) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n :=
-  dvd_rfl.pow hn
-#align dvd_pow_self dvd_pow_self
-
 end Monoid
 
 lemma eq_zero_or_one_of_sq_eq_self [CancelMonoidWithZero M] {x : M} (hx : x ^ 2 = x) :
@@ -254,29 +241,14 @@ lemma eq_zero_or_one_of_sq_eq_self [CancelMonoidWithZero M] {x : M} (hx : x ^ 2
 -/
 
 section CommMonoid
-
-variable [CommMonoid M] [AddCommMonoid A]
+variable [CommMonoid M]
 
 @[to_additive nsmul_add]
 theorem mul_pow (a b : M) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n :=
   (Commute.all a b).mul_pow n
 #align mul_pow mul_pow
 #align nsmul_add nsmul_add
 
-/-- The `n`th power map on a commutative monoid for a natural `n`, considered as a morphism of
-monoids. -/
-@[to_additive (attr := simps)
-      "Multiplication by a natural `n` on a commutative additive
-       monoid, considered as a morphism of additive monoids."]
-def powMonoidHom (n : ℕ) : M →* M where
-  toFun := (· ^ n)
-  map_one' := one_pow _
-  map_mul' a b := mul_pow a b n
-#align pow_monoid_hom powMonoidHom
-#align nsmul_add_monoid_hom nsmulAddMonoidHom
-#align pow_monoid_hom_apply powMonoidHom_apply
-#align nsmul_add_monoid_hom_apply nsmulAddMonoidHom_apply
-
 end CommMonoid
 
 section DivInvMonoid
@@ -403,20 +375,6 @@ theorem div_zpow (a b : α) (n : ℤ) : (a / b) ^ n = a ^ n / b ^ n := by
 #align div_zpow div_zpow
 #align zsmul_sub zsmul_sub
 
-/-- The `n`-th power map (for an integer `n`) on a commutative group, considered as a group
-homomorphism. -/
-@[to_additive (attr := simps)
-      "Multiplication by an integer `n` on a commutative additive group, considered as an
-       additive group homomorphism."]
-def zpowGroupHom (n : ℤ) : α →* α where
-  toFun := (· ^ n)
-  map_one' := one_zpow n
-  map_mul' a b := mul_zpow a b n
-#align zpow_group_hom zpowGroupHom
-#align zsmul_add_group_hom zsmulAddGroupHom
-#align zpow_group_hom_apply zpowGroupHom_apply
-#align zsmul_add_group_hom_apply zsmulAddGroupHom_apply
-
 end DivisionCommMonoid
 
 section Group
@@ -443,10 +401,6 @@ theorem inv_pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^
 
 end Group
 
-theorem pow_dvd_pow [Monoid R] (a : R) {m n : ℕ} (h : m ≤ n) : a ^ m ∣ a ^ n :=
-  ⟨a ^ (n - m), by rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]⟩
-#align pow_dvd_pow pow_dvd_pow
-
 @[to_additive (attr := simp)]
 theorem SemiconjBy.zpow_right [Group G] {a x y : G} (h : SemiconjBy a x y) :
     ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)

Mathlib/Algebra/GroupPower/Hom.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2021 Kevin Buzzard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Buzzard
+-/
+import Mathlib.Algebra.GroupPower.Basic
+import Mathlib.Algebra.Group.Hom.Defs
+
+/-!
+# Power as a monoid hom
+-/
+
+variable {α : Type*}
+
+section CommMonoid
+variable [CommMonoid α]
+
+/-- The `n`th power map on a commutative monoid for a natural `n`, considered as a morphism of
+monoids. -/
+@[to_additive (attr := simps) "Multiplication by a natural `n` on a commutative additive monoid,
+considered as a morphism of additive monoids."]
+def powMonoidHom (n : ℕ) : α →* α where
+  toFun := (· ^ n)
+  map_one' := one_pow _
+  map_mul' a b := mul_pow a b n
+#align pow_monoid_hom powMonoidHom
+#align nsmul_add_monoid_hom nsmulAddMonoidHom
+#align pow_monoid_hom_apply powMonoidHom_apply
+#align nsmul_add_monoid_hom_apply nsmulAddMonoidHom_apply
+
+end CommMonoid
+
+section DivisionCommMonoid
+variable [DivisionCommMonoid α]
+
+/-- The `n`-th power map (for an integer `n`) on a commutative group, considered as a group
+homomorphism. -/
+@[to_additive (attr := simps) "Multiplication by an integer `n` on a commutative additive group,
+considered as an additive group homomorphism."]
+def zpowGroupHom (n : ℤ) : α →* α where
+  toFun := (· ^ n)
+  map_one' := one_zpow n
+  map_mul' a b := mul_zpow a b n
+#align zpow_group_hom zpowGroupHom
+#align zsmul_add_group_hom zsmulAddGroupHom
+#align zpow_group_hom_apply zpowGroupHom_apply
+#align zsmul_add_group_hom_apply zsmulAddGroupHom_apply
+
+end DivisionCommMonoid

Mathlib/Algebra/GroupPower/Order.lean

@@ -167,9 +167,7 @@ theorem pow_lt_self_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n
   simpa only [pow_one] using pow_lt_pow_right_of_lt_one h₀ h₁ hn
 #align pow_lt_self_of_lt_one pow_lt_self_of_lt_one
 
-theorem sq_pos_of_pos (ha : 0 < a) : 0 < a ^ 2 := by
-  rw [sq]
-  exact mul_pos ha ha
+theorem sq_pos_of_pos (ha : 0 < a) : 0 < a ^ 2 := pow_pos ha _
 #align sq_pos_of_pos sq_pos_of_pos
 
 end StrictOrderedSemiring
@@ -297,10 +295,6 @@ theorem pow_bit0_nonneg (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n := by
   exact mul_self_nonneg _
 #align pow_bit0_nonneg pow_bit0_nonneg
 
-theorem sq_nonneg (a : R) : 0 ≤ a ^ 2 :=
-  pow_bit0_nonneg a 1
-#align sq_nonneg sq_nonneg
-
 alias pow_two_nonneg := sq_nonneg
 #align pow_two_nonneg pow_two_nonneg
 
@@ -402,20 +396,6 @@ theorem pow_four_le_pow_two_of_pow_two_le {x y : R} (h : x ^ 2 ≤ y) : x ^ 4 
 
 end LinearOrderedRing
 
-section LinearOrderedCommRing
-
-variable [LinearOrderedCommRing R]
-
-/-- Arithmetic mean-geometric mean (AM-GM) inequality for linearly ordered commutative rings. -/
-theorem two_mul_le_add_sq (a b : R) : 2 * a * b ≤ a ^ 2 + b ^ 2 :=
-  sub_nonneg.mp ((sub_add_eq_add_sub _ _ _).subst ((sub_sq a b).subst (sq_nonneg _)))
-#align two_mul_le_add_sq two_mul_le_add_sq
-
-alias two_mul_le_add_pow_two := two_mul_le_add_sq
-#align two_mul_le_add_pow_two two_mul_le_add_pow_two
-
-end LinearOrderedCommRing
-
 section LinearOrderedCommMonoidWithZero
 
 variable [LinearOrderedCommMonoidWithZero M] [NoZeroDivisors M] {a : M} {n : ℕ}

Mathlib/Algebra/GroupPower/Ring.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 
 import Mathlib.Algebra.Group.Units.Hom
-import Mathlib.Algebra.GroupPower.Basic
+import Mathlib.Algebra.GroupPower.Hom
 import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Ring.Commute

Mathlib/Algebra/Order/Monoid/MinMax.lean

@@ -20,20 +20,29 @@ variable {α β : Type*}
 /-! Some lemmas about types that have an ordering and a binary operation, with no
   rules relating them. -/
 
+section CommSemigroup
+variable[LinearOrder α] [CommSemigroup α] [CommSemigroup β]
 
 @[to_additive]
-theorem fn_min_mul_fn_max [LinearOrder α] [CommSemigroup β] (f : α → β) (n m : α) :
-    f (min n m) * f (max n m) = f n * f m := by
-  rcases le_total n m with h | h <;> simp [h, mul_comm]
+lemma fn_min_mul_fn_max  (f : α → β) (a b : α) : f (min a b) * f (max a b) = f a * f b := by
+  obtain h | h := le_total a b <;> simp [h, mul_comm]
 #align fn_min_mul_fn_max fn_min_mul_fn_max
 #align fn_min_add_fn_max fn_min_add_fn_max
 
 @[to_additive]
-theorem min_mul_max [LinearOrder α] [CommSemigroup α] (n m : α) : min n m * max n m = n * m :=
-  fn_min_mul_fn_max id n m
+lemma fn_max_mul_fn_min (f : α → β) (a b : α) : f (max a b) * f (min a b) = f a * f b := by
+  obtain h | h := le_total a b <;> simp [h, mul_comm]
+
+@[to_additive (attr := simp)]
+lemma min_mul_max (a b : α) : min a b * max a b = a * b := fn_min_mul_fn_max id _ _
 #align min_mul_max min_mul_max
 #align min_add_max min_add_max
 
+@[to_additive (attr := simp)]
+lemma max_mul_min (a b : α) : max a b * min a b = a * b := fn_max_mul_fn_min id _ _
+
+end CommSemigroup
+
 section CovariantClassMulLe
 
 variable [LinearOrder α]

Mathlib/Algebra/Order/Ring/Canonical.lean

@@ -5,7 +5,6 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Order.Sub.Canonical
-import Mathlib.GroupTheory.GroupAction.Defs
 
 #align_import algebra.order.ring.canonical from "leanprover-community/mathlib"@"824f9ae93a4f5174d2ea948e2d75843dd83447bb"
 
@@ -39,64 +38,6 @@ class CanonicallyOrderedCommSemiring (α : Type*) extends CanonicallyOrderedAddC
   protected eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : α}, a * b = 0 → a = 0 ∨ b = 0
 #align canonically_ordered_comm_semiring CanonicallyOrderedCommSemiring
 
-section StrictOrderedSemiring
-
-variable [StrictOrderedSemiring α] {a b c d : α}
-
-section ExistsAddOfLE
-
-variable [ExistsAddOfLE α]
-
-/-- Binary **rearrangement inequality**. -/
-theorem mul_add_mul_le_mul_add_mul (hab : a ≤ b) (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d := by
-  obtain ⟨b, rfl⟩ := exists_add_of_le hab
-  obtain ⟨d, rfl⟩ := exists_add_of_le hcd
-  rw [mul_add, add_right_comm, mul_add, ← add_assoc]
-  exact add_le_add_left (mul_le_mul_of_nonneg_right hab <| (le_add_iff_nonneg_right _).1 hcd) _
-#align mul_add_mul_le_mul_add_mul mul_add_mul_le_mul_add_mul
-
-/-- Binary **rearrangement inequality**. -/
-theorem mul_add_mul_le_mul_add_mul' (hba : b ≤ a) (hdc : d ≤ c) :
-    a • d + b • c ≤ a • c + b • d := by
-  rw [add_comm (a • d), add_comm (a • c)]
-  exact mul_add_mul_le_mul_add_mul hba hdc
-#align mul_add_mul_le_mul_add_mul' mul_add_mul_le_mul_add_mul'
-
-/-- Binary strict **rearrangement inequality**. -/
-theorem mul_add_mul_lt_mul_add_mul (hab : a < b) (hcd : c < d) : a * d + b * c < a * c + b * d := by
-  obtain ⟨b, rfl⟩ := exists_add_of_le hab.le
-  obtain ⟨d, rfl⟩ := exists_add_of_le hcd.le
-  rw [mul_add, add_right_comm, mul_add, ← add_assoc]
-  exact add_lt_add_left (mul_lt_mul_of_pos_right hab <| (lt_add_iff_pos_right _).1 hcd) _
-#align mul_add_mul_lt_mul_add_mul mul_add_mul_lt_mul_add_mul
-
-/-- Binary **rearrangement inequality**. -/
-theorem mul_add_mul_lt_mul_add_mul' (hba : b < a) (hdc : d < c) :
-    a • d + b • c < a • c + b • d := by
-  rw [add_comm (a • d), add_comm (a • c)]
-  exact mul_add_mul_lt_mul_add_mul hba hdc
-#align mul_add_mul_lt_mul_add_mul' mul_add_mul_lt_mul_add_mul'
-
-end ExistsAddOfLE
-
-end StrictOrderedSemiring
-
-section LinearOrderedCommSemiring
-variable [LinearOrderedCommSemiring α] [ExistsAddOfLE α] {a b : α}
-
-lemma add_sq_le : (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2) := by
-  calc
-    (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a) := by
-        simp_rw [pow_succ, pow_zero, mul_one, add_mul_self_eq, mul_assoc, two_mul,
-          add_right_comm _ (_ + _), mul_comm]
-    _ ≤ a ^ 2 + b ^ 2 + (a * a + b * b) := add_le_add_left ?_ _
-    _ = _ := by simp_rw [pow_succ, pow_zero, mul_one, two_mul]
-  cases le_total a b
-  · exact mul_add_mul_le_mul_add_mul ‹_› ‹_›
-  · exact mul_add_mul_le_mul_add_mul' ‹_› ‹_›
-
-end LinearOrderedCommSemiring
-
 namespace CanonicallyOrderedCommSemiring
 
 variable [CanonicallyOrderedCommSemiring α] {a b c d : α}