chore(Algebra/Regular/Basic): generalize to IsCancelMul (#8428)

This lets lemmas about cancellative monoids work for cancellative semigroups

Some docstrings have been rewritten, as adjusting the wording was too awkward.

The new `.all` names are intended to match `Commute.all`.

Author: eric-wieser

Mathlib/Algebra/CovariantAndContravariant.lean

@@ -31,7 +31,7 @@ relation (typically `(≤)` or `(<)`), these are the only two typeclasses that I
 The general approach is to formulate the lemma that you are interested in and prove it, with the
 `Ordered[...]` typeclass of your liking.  After that, you convert the single typeclass,
 say `[OrderedCancelMonoid M]`, into three typeclasses, e.g.
-`[LeftCancelSemigroup M] [PartialOrder M] [CovariantClass M M (Function.swap (*)) (≤)]`
+`[CancelMonoid M] [PartialOrder M] [CovariantClass M M (Function.swap (*)) (≤)]`
 and have a go at seeing if the proof still works!
 
 Note that it is possible to combine several `Co(ntra)variantClass` assumptions together.
@@ -362,27 +362,27 @@ theorem contravariant_le_of_contravariant_eq_and_lt [PartialOrder N]
   then the following four instances (actually eight) can be removed in favor of the above two. -/
 
 @[to_additive]
-instance LeftCancelSemigroup.covariant_mul_lt_of_covariant_mul_le [LeftCancelSemigroup N]
+instance IsLeftCancelMul.covariant_mul_lt_of_covariant_mul_le [Mul N] [IsLeftCancelMul N]
     [PartialOrder N] [CovariantClass N N (· * ·) (· ≤ ·)] :
     CovariantClass N N (· * ·) (· < ·) where
   elim a _ _ bc := (CovariantClass.elim a bc.le).lt_of_ne ((mul_ne_mul_right a).mpr bc.ne)
 
 @[to_additive]
-instance RightCancelSemigroup.covariant_swap_mul_lt_of_covariant_swap_mul_le
-    [RightCancelSemigroup N] [PartialOrder N] [CovariantClass N N (swap (· * ·)) (· ≤ ·)] :
+instance IsRightCancelMul.covariant_swap_mul_lt_of_covariant_swap_mul_le
+    [Mul N] [IsRightCancelMul N] [PartialOrder N] [CovariantClass N N (swap (· * ·)) (· ≤ ·)] :
     CovariantClass N N (swap (· * ·)) (· < ·) where
   elim a _ _ bc := (CovariantClass.elim a bc.le).lt_of_ne ((mul_ne_mul_left a).mpr bc.ne)
 
 @[to_additive]
-instance LeftCancelSemigroup.contravariant_mul_le_of_contravariant_mul_lt [LeftCancelSemigroup N]
+instance IsLeftCancelMul.contravariant_mul_le_of_contravariant_mul_lt [Mul N] [IsLeftCancelMul N]
     [PartialOrder N] [ContravariantClass N N (· * ·) (· < ·)] :
     ContravariantClass N N (· * ·) (· ≤ ·) where
   elim := (contravariant_le_iff_contravariant_lt_and_eq N N _).mpr
     ⟨ContravariantClass.elim, fun _ ↦ mul_left_cancel⟩
 
 @[to_additive]
-instance RightCancelSemigroup.contravariant_swap_mul_le_of_contravariant_swap_mul_lt
-    [RightCancelSemigroup N] [PartialOrder N] [ContravariantClass N N (swap (· * ·)) (· < ·)] :
+instance IsRightCancelMul.contravariant_swap_mul_le_of_contravariant_swap_mul_lt
+    [Mul N] [IsRightCancelMul N] [PartialOrder N] [ContravariantClass N N (swap (· * ·)) (· < ·)] :
     ContravariantClass N N (swap (· * ·)) (· ≤ ·) where
   elim := (contravariant_le_iff_contravariant_lt_and_eq N N _).mpr
     ⟨ContravariantClass.elim, fun _ ↦ mul_right_cancel⟩

Mathlib/Algebra/Group/Embedding.lean

@@ -13,31 +13,29 @@ import Mathlib.Logic.Embedding.Basic
 -/
 
 
-variable {R : Type*}
+variable {G : Type*}
 
 section LeftOrRightCancelSemigroup
 
-/-- The embedding of a left cancellative semigroup into itself
-by left multiplication by a fixed element.
- -/
+/-- If left-multiplication by any element is cancellative, left-multiplication by `g` is an
+embedding. -/
 @[to_additive (attr := simps)
-      "The embedding of a left cancellative additive semigroup into itself
-         by left translation by a fixed element." ]
-def mulLeftEmbedding {G : Type*} [LeftCancelSemigroup G] (g : G) : G ↪ G where
+      "If left-addition by any element is cancellative, left-addition by `g` is an
+        embedding."]
+def mulLeftEmbedding [Mul G] [IsLeftCancelMul G] (g : G) : G ↪ G where
   toFun h := g * h
   inj' := mul_right_injective g
 #align mul_left_embedding mulLeftEmbedding
 #align add_left_embedding addLeftEmbedding
 #align add_left_embedding_apply addLeftEmbedding_apply
 #align mul_left_embedding_apply mulLeftEmbedding_apply
 
-/-- The embedding of a right cancellative semigroup into itself
-by right multiplication by a fixed element.
- -/
+/-- If right-multiplication by any element is cancellative, right-multiplication by `g` is an
+embedding. -/
 @[to_additive (attr := simps)
-      "The embedding of a right cancellative additive semigroup into itself
-         by right translation by a fixed element."]
-def mulRightEmbedding {G : Type*} [RightCancelSemigroup G] (g : G) : G ↪ G where
+      "If right-addition by any element is cancellative, right-addition by `g` is an
+        embedding."]
+def mulRightEmbedding [Mul G] [IsRightCancelMul G] (g : G) : G ↪ G where
   toFun h := h * g
   inj' := mul_left_injective g
 #align mul_right_embedding mulRightEmbedding
@@ -46,7 +44,7 @@ def mulRightEmbedding {G : Type*} [RightCancelSemigroup G] (g : G) : G ↪ G whe
 #align add_right_embedding_apply addRightEmbedding_apply
 
 @[to_additive]
-theorem mulLeftEmbedding_eq_mulRightEmbedding {G : Type*} [CancelCommMonoid G] (g : G) :
+theorem mulLeftEmbedding_eq_mulRightEmbedding [CommSemigroup G] [IsCancelMul G] (g : G) :
     mulLeftEmbedding g = mulRightEmbedding g := by
   ext
   exact mul_comm _ _

Mathlib/Algebra/MonoidAlgebra/Support.lean

@@ -79,21 +79,21 @@ theorem support_mul [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) :
       Subset.trans support_sum <| biUnion_mono fun _a₂ _ => support_single_subset
 #align monoid_algebra.support_mul MonoidAlgebra.support_mul
 
-theorem support_mul_single [RightCancelSemigroup G] (f : MonoidAlgebra k G) (r : k)
+theorem support_mul_single [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k)
     (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
     (f * single x r).support = f.support.map (mulRightEmbedding x) := by
   classical
     ext
-    simp only [support_mul_single_eq_image f hr (isRightRegular_of_rightCancelSemigroup x),
+    simp only [support_mul_single_eq_image f hr (IsRightRegular.all x),
       mem_image, mem_map, mulRightEmbedding_apply]
 #align monoid_algebra.support_mul_single MonoidAlgebra.support_mul_single
 
-theorem support_single_mul [LeftCancelSemigroup G] (f : MonoidAlgebra k G) (r : k)
+theorem support_single_mul [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) (r : k)
     (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
     (single x r * f : MonoidAlgebra k G).support = f.support.map (mulLeftEmbedding x) := by
   classical
     ext
-    simp only [support_single_mul_eq_image f hr (isLeftRegular_of_leftCancelSemigroup x), mem_image,
+    simp only [support_single_mul_eq_image f hr (IsLeftRegular.all x), mem_image,
       mem_map, mulLeftEmbedding_apply]
 #align monoid_algebra.support_single_mul MonoidAlgebra.support_single_mul
 
@@ -122,16 +122,16 @@ theorem support_mul [DecidableEq G] [Add G] (a b : k[G]) :
   @MonoidAlgebra.support_mul k (Multiplicative G) _ _ _ _ _
 #align add_monoid_algebra.support_mul AddMonoidAlgebra.support_mul
 
-theorem support_mul_single [AddRightCancelSemigroup G] (f : k[G]) (r : k)
+theorem support_mul_single [Add G] [IsRightCancelAdd G] (f : k[G]) (r : k)
     (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
     (f * single x r : k[G]).support = f.support.map (addRightEmbedding x) :=
-  @MonoidAlgebra.support_mul_single k (Multiplicative G) _ _ _ _ hr _
+  MonoidAlgebra.support_mul_single (G := Multiplicative G) _ _ hr _
 #align add_monoid_algebra.support_mul_single AddMonoidAlgebra.support_mul_single
 
-theorem support_single_mul [AddLeftCancelSemigroup G] (f : k[G]) (r : k)
+theorem support_single_mul [Add G] [IsLeftCancelAdd G] (f : k[G]) (r : k)
     (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
     (single x r * f : k[G]).support = f.support.map (addLeftEmbedding x) :=
-  @MonoidAlgebra.support_single_mul k (Multiplicative G) _ _ _ _ hr _
+  MonoidAlgebra.support_single_mul (G := Multiplicative G) _ _ hr _
 #align add_monoid_algebra.support_single_mul AddMonoidAlgebra.support_single_mul
 
 section Span

Mathlib/Algebra/Order/Group/Defs.lean

@@ -60,7 +60,7 @@ instance (priority := 100) OrderedCommGroup.toOrderedCancelCommMonoid [OrderedCo
 #align ordered_add_comm_group.to_ordered_cancel_add_comm_monoid OrderedAddCommGroup.toOrderedCancelAddCommMonoid
 
 example (α : Type u) [OrderedAddCommGroup α] : CovariantClass α α (swap (· + ·)) (· < ·) :=
-  AddRightCancelSemigroup.covariant_swap_add_lt_of_covariant_swap_add_le α
+  IsRightCancelAdd.covariant_swap_add_lt_of_covariant_swap_add_le α
 
 -- Porting note: this instance is not used,
 -- and causes timeouts after lean4#2210.

Mathlib/Algebra/Order/WithZero.lean

@@ -208,7 +208,7 @@ theorem mul_lt_right₀ (c : α) (h : a < b) (hc : c ≠ 0) : a * c < b * c := b
 theorem inv_lt_inv₀ (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ < b⁻¹ ↔ b < a :=
   show (Units.mk0 a ha)⁻¹ < (Units.mk0 b hb)⁻¹ ↔ Units.mk0 b hb < Units.mk0 a ha from
     have : CovariantClass αˣ αˣ (· * ·) (· < ·) :=
-      LeftCancelSemigroup.covariant_mul_lt_of_covariant_mul_le αˣ
+      IsLeftCancelMul.covariant_mul_lt_of_covariant_mul_le αˣ
     inv_lt_inv_iff
 #align inv_lt_inv₀ inv_lt_inv₀
 

Mathlib/Algebra/Regular/Basic.lean

@@ -343,35 +343,26 @@ theorem IsUnit.isRegular (ua : IsUnit a) : IsRegular a := by
 
 end Monoid
 
-/-- Elements of a left cancel semigroup are left regular. -/
-@[to_additive "Elements of an add left cancel semigroup are add-left-regular."]
-theorem isLeftRegular_of_leftCancelSemigroup [LeftCancelSemigroup R]
-    (g : R) : IsLeftRegular g :=
+/-- If all multiplications cancel on the left then every element is left-regular. -/
+@[to_additive "If all additions cancel on the left then every element is add-left-regular."]
+theorem IsLeftRegular.all [Mul R] [IsLeftCancelMul R] (g : R) : IsLeftRegular g :=
   mul_right_injective g
-#align is_left_regular_of_left_cancel_semigroup isLeftRegular_of_leftCancelSemigroup
-#align is_add_left_regular_of_left_cancel_add_semigroup isAddLeftRegular_of_addLeftCancelSemigroup
+#align is_left_regular_of_left_cancel_semigroup IsLeftRegular.all
+#align is_add_left_regular_of_left_cancel_add_semigroup IsAddLeftRegular.all
 
-/-- Elements of a right cancel semigroup are right regular. -/
-@[to_additive "Elements of an add right cancel semigroup are add-right-regular"]
-theorem isRightRegular_of_rightCancelSemigroup [RightCancelSemigroup R]
-    (g : R) : IsRightRegular g :=
+/-- If all multiplications cancel on the right then every element is right-regular. -/
+@[to_additive "If all additions cancel on the right then every element is add-right-regular."]
+theorem IsRightRegular.all [Mul R] [IsRightCancelMul R] (g : R) : IsRightRegular g :=
   mul_left_injective g
-#align is_right_regular_of_right_cancel_semigroup isRightRegular_of_rightCancelSemigroup
-#align is_add_right_regular_of_right_cancel_add_semigroup   isAddRightRegular_of_addRightCancelSemigroup
+#align is_right_regular_of_right_cancel_semigroup IsRightRegular.all
+#align is_add_right_regular_of_right_cancel_add_semigroup IsLeftRegular.all
 
-section CancelMonoid
-
-variable [CancelMonoid R]
-
-/-- Elements of a cancel monoid are regular.  Cancel semigroups do not appear to exist. -/
-@[to_additive "Elements of an add cancel monoid are regular.
-Add cancel semigroups do not appear to exist."]
-theorem isRegular_of_cancelMonoid (g : R) : IsRegular g :=
+/-- If all multiplications cancel then every element is regular. -/
+@[to_additive "If all additions cancel then every element is add-regular."]
+theorem IsRegular.all [Mul R] [IsCancelMul R] (g : R) : IsRegular g :=
   ⟨mul_right_injective g, mul_left_injective g⟩
-#align is_regular_of_cancel_monoid isRegular_of_cancelMonoid
-#align is_add_regular_of_cancel_add_monoid isAddRegular_of_addCancelMonoid
-
-end CancelMonoid
+#align is_regular_of_cancel_monoid IsRegular.all
+#align is_add_regular_of_cancel_add_monoid IsAddRegular.all
 
 section CancelMonoidWithZero
 

Mathlib/Data/Finset/Pointwise.lean

@@ -1869,9 +1869,9 @@ theorem op_smul_finset_mul_eq_mul_smul_finset (a : α) (s : Finset α) (t : Fins
 
 end Semigroup
 
-section LeftCancelSemigroup
+section IsLeftCancelMul
 
-variable [LeftCancelSemigroup α] [DecidableEq α] (s t : Finset α) (a : α)
+variable [Mul α] [IsLeftCancelMul α] [DecidableEq α] (s t : Finset α) (a : α)
 
 @[to_additive]
 theorem pairwiseDisjoint_smul_iff {s : Set α} {t : Finset α} :
@@ -1898,11 +1898,11 @@ theorem card_le_card_mul_left {s : Finset α} (hs : s.Nonempty) : t.card ≤ (s
 #align finset.card_le_card_mul_left Finset.card_le_card_mul_left
 #align finset.card_le_card_add_left Finset.card_le_card_add_left
 
-end LeftCancelSemigroup
+end IsLeftCancelMul
 
 section
 
-variable [RightCancelSemigroup α] [DecidableEq α] (s t : Finset α) (a : α)
+variable [Mul α] [IsRightCancelMul α] [DecidableEq α] (s t : Finset α) (a : α)
 
 @[to_additive (attr := simp)]
 theorem card_mul_singleton : (s * {a}).card = s.card :=

Mathlib/Data/Set/Pointwise/SMul.lean

@@ -857,9 +857,9 @@ theorem op_smul_set_mul_eq_mul_smul_set (a : α) (s : Set α) (t : Set α) :
 
 end Semigroup
 
-section LeftCancelSemigroup
+section IsLeftCancelMul
 
-variable [LeftCancelSemigroup α] {s t : Set α}
+variable [Mul α] [IsLeftCancelMul α] {s t : Set α}
 
 @[to_additive]
 theorem pairwiseDisjoint_smul_iff :
@@ -868,7 +868,7 @@ theorem pairwiseDisjoint_smul_iff :
 #align set.pairwise_disjoint_smul_iff Set.pairwiseDisjoint_smul_iff
 #align set.pairwise_disjoint_vadd_iff Set.pairwiseDisjoint_vadd_iff
 
-end LeftCancelSemigroup
+end IsLeftCancelMul
 
 section Group