diff --git a/src/algebra/group/to_additive.lean b/src/algebra/group/to_additive.lean
index 2144758a97c29..8de9b01f245f6 100644
--- a/src/algebra/group/to_additive.lean
+++ b/src/algebra/group/to_additive.lean
@@ -217,7 +217,12 @@ meta def tr : bool → list string → list string
 | is_comm ("pow" :: s)                := add_comm_prefix is_comm "nsmul"     :: tr ff s
 | is_comm ("npow" :: s)               := add_comm_prefix is_comm "nsmul"     :: tr ff s
 | is_comm ("zpow" :: s)               := add_comm_prefix is_comm "zsmul"     :: tr ff s
-| is_comm ("is" :: "square" :: s)             := add_comm_prefix is_comm "even"      :: tr ff s
+| is_comm ("is" :: "square" :: s)     := add_comm_prefix is_comm "even"      :: tr ff s
+| is_comm ("is" :: "regular" :: s)    := add_comm_prefix is_comm "is_add_regular"   :: tr ff s
+| is_comm ("is" :: "left" :: "regular" :: s)  :=
+  add_comm_prefix is_comm "is_add_left_regular"  :: tr ff s
+| is_comm ("is" :: "right" :: "regular" :: s) :=
+  add_comm_prefix is_comm "is_add_right_regular" :: tr ff s
 | is_comm ("monoid" :: s)      := ("add_" ++ add_comm_prefix is_comm "monoid")    :: tr ff s
 | is_comm ("submonoid" :: s)   := ("add_" ++ add_comm_prefix is_comm "submonoid") :: tr ff s
 | is_comm ("group" :: s)       := ("add_" ++ add_comm_prefix is_comm "group")     :: tr ff s
diff --git a/src/algebra/regular/basic.lean b/src/algebra/regular/basic.lean
index ba91b6aacdbe2..75f5a84ab02a1 100644
--- a/src/algebra/regular/basic.lean
+++ b/src/algebra/regular/basic.lean
@@ -10,7 +10,8 @@ import logic.embedding
 /-!
 # Regular elements
 
-We introduce left-regular, right-regular and regular elements.
+We introduce left-regular, right-regular and regular elements, along with their `to_additive`
+analogues add-left-regular, add-right-regular and add-regular elements.
 
 By definition, a regular element in a commutative ring is a non-zero divisor.
 Lemma `is_regular_of_ne_zero` implies that every non-zero element of an integral domain is regular.
@@ -30,19 +31,33 @@ section has_mul
 variable [has_mul R]
 
 /-- A left-regular element is an element `c` such that multiplication on the left by `c`
-is injective on the left. -/
+is injective. -/
+@[to_additive "An add-left-regular element is an element `c` such that addition on the left by `c`
+is injective. -/
+"]
 def is_left_regular (c : R) := function.injective ((*) c)
 
 /-- A right-regular element is an element `c` such that multiplication on the right by `c`
-is injective on the right. -/
+is injective. -/
+@[to_additive "An add-right-regular element is an element `c` such that addition on the right by `c`
+is injective."]
 def is_right_regular (c : R) := function.injective (* c)
 
+/-- An add-regular element is an element `c` such that addition by `c` both on the left and
+on the right is injective. -/
+structure is_add_regular {R : Type*} [has_add R] (c : R) : Prop :=
+(left : is_add_left_regular c)
+(right : is_add_right_regular c)
+
 /-- A regular element is an element `c` such that multiplication by `c` both on the left and
 on the right is injective. -/
 structure is_regular (c : R) : Prop :=
 (left : is_left_regular c)
 (right : is_right_regular c)
 
+attribute [to_additive] is_regular
+
+@[to_additive]
 protected lemma mul_le_cancellable.is_left_regular [partial_order R] {a : R}
   (ha : mul_le_cancellable a) : is_left_regular a :=
 ha.injective
@@ -62,29 +77,38 @@ section semigroup
 variable [semigroup R]
 
 /-- In a semigroup, the product of left-regular elements is left-regular. -/
+@[to_additive "In an additive semigroup, the sum of add-left-regular elements is add-left.regular."]
 lemma is_left_regular.mul (lra : is_left_regular a) (lrb : is_left_regular b) :
   is_left_regular (a * b) :=
 show function.injective ((*) (a * b)), from (comp_mul_left a b) ▸ lra.comp lrb
 
 /-- In a semigroup, the product of right-regular elements is right-regular. -/
+@[to_additive
+"In an additive semigroup, the sum of add-right-regular elements is add-right-regular."]
 lemma is_right_regular.mul (rra : is_right_regular a) (rrb : is_right_regular b) :
   is_right_regular (a * b) :=
 show function.injective (* (a * b)), from (comp_mul_right b a) ▸ rrb.comp rra
 
 /--  If an element `b` becomes left-regular after multiplying it on the left by a left-regular
 element, then `b` is left-regular. -/
+@[to_additive "If an element `b` becomes add-left-regular after adding to it on the left a
+add-left-regular element, then `b` is add-left-regular."]
 lemma is_left_regular.of_mul (ab : is_left_regular (a * b)) :
   is_left_regular b :=
 function.injective.of_comp (by rwa comp_mul_left a b)
 
 /--  An element is left-regular if and only if multiplying it on the left by a left-regular element
 is left-regular. -/
-@[simp] lemma mul_is_left_regular_iff (b : R) (ha : is_left_regular a) :
+@[simp, to_additive "An element is add-left-regular if and only if adding to it on the left a
+add-left-regular element is add-left-regular."]
+lemma mul_is_left_regular_iff (b : R) (ha : is_left_regular a) :
   is_left_regular (a * b) ↔ is_left_regular b :=
 ⟨λ ab, is_left_regular.of_mul ab, λ ab, is_left_regular.mul ha ab⟩
 
 /--  If an element `b` becomes right-regular after multiplying it on the right by a right-regular
 element, then `b` is right-regular. -/
+@[to_additive "If an element `b` becomes add-right-regular after adding to it on the right a
+add-right-regular element, then `b` is add-right-regular."]
 lemma is_right_regular.of_mul (ab : is_right_regular (b * a)) :
   is_right_regular b :=
 begin
@@ -95,12 +119,16 @@ end
 
 /--  An element is right-regular if and only if multiplying it on the right with a right-regular
 element is right-regular. -/
-@[simp] lemma mul_is_right_regular_iff (b : R) (ha : is_right_regular a) :
+@[simp, to_additive "An element is add-right-regular if and only if adding it on the right to a
+add-right-regular element is add-right-regular."]
+lemma mul_is_right_regular_iff (b : R) (ha : is_right_regular a) :
   is_right_regular (b * a) ↔ is_right_regular b :=
 ⟨λ ab, is_right_regular.of_mul ab, λ ab, is_right_regular.mul ab ha⟩
 
 /--  Two elements `a` and `b` are regular if and only if both products `a * b` and `b * a`
 are regular. -/
+@[to_additive "Two elements `a` and `b` are add-regular if and only if both sums `a + b` and `b + a`
+are add-regular."]
 lemma is_regular_mul_and_mul_iff :
   is_regular (a * b) ∧ is_regular (b * a) ↔ is_regular a ∧ is_regular b :=
 begin
@@ -116,6 +144,8 @@ begin
 end
 
 /--  The "most used" implication of `mul_and_mul_iff`, with split hypotheses, instead of `∧`. -/
+@[to_additive "The \"most used\" implication of `add_and_add_iff`, with split hypotheses,
+instead of `∧`."]
 lemma is_regular.and_of_mul_of_mul (ab : is_regular (a * b)) (ba : is_regular (b * a)) :
   is_regular a ∧ is_regular b :=
 is_regular_mul_and_mul_iff.mp ⟨ab, ba⟩
@@ -216,6 +246,7 @@ section comm_semigroup
 variable [comm_semigroup R]
 
 /--  A product is regular if and only if the factors are. -/
+@[to_additive "A sum is add-regular if and only if the summands are."]
 lemma is_regular_mul_iff : is_regular (a * b) ↔ is_regular a ∧ is_regular b :=
 begin
   refine iff.trans _ is_regular_mul_and_mul_iff,
@@ -229,23 +260,28 @@ section monoid
 variables [monoid R]
 
 /--  In a monoid, `1` is regular. -/
+@[to_additive "In an additive monoid, `0` is regular."]
 lemma is_regular_one : is_regular (1 : R) :=
 ⟨λ a b ab, (one_mul a).symm.trans (eq.trans ab (one_mul b)),
   λ a b ab, (mul_one a).symm.trans (eq.trans ab (mul_one b))⟩
 
 /-- An element admitting a left inverse is left-regular. -/
+@[to_additive "An element admitting a left additive opposite is add-left-regular."]
 lemma is_left_regular_of_mul_eq_one (h : b * a = 1) : is_left_regular a :=
 @is_left_regular.of_mul R _ a _ (by { rw h, exact is_regular_one.left })
 
 /-- An element admitting a right inverse is right-regular. -/
+@[to_additive "An element admitting a right additive opposite is add-right-regular."]
 lemma is_right_regular_of_mul_eq_one (h : a * b = 1) : is_right_regular a :=
 @is_right_regular.of_mul R _ a _ (by { rw h, exact is_regular_one.right })
 
 /-- If `R` is a monoid, an element in `Rˣ` is regular. -/
+@[to_additive "If `R` is an additive monoid, an element in `add_units R` is add-regular."]
 lemma units.is_regular (a : Rˣ) : is_regular (a : R) :=
 ⟨is_left_regular_of_mul_eq_one a.inv_mul, is_right_regular_of_mul_eq_one a.mul_inv⟩
 
 /-- A unit in a monoid is regular. -/
+@[to_additive "An additive unit in an additive monoid is add-regular."]
 lemma is_unit.is_regular (ua : is_unit a) : is_regular a :=
 begin
   rcases ua with ⟨a, rfl⟩,
@@ -282,11 +318,13 @@ lemma mul_left_embedding_eq_mul_right_embedding {G : Type*} [cancel_comm_monoid
 by { ext, exact mul_comm _ _ }
 
 /--  Elements of a left cancel semigroup are left regular. -/
+@[to_additive "Elements of an add left cancel semigroup are add-left-regular."]
 lemma is_left_regular_of_left_cancel_semigroup [left_cancel_semigroup R] (g : R) :
   is_left_regular g :=
 mul_right_injective g
 
 /--  Elements of a right cancel semigroup are right regular. -/
+@[to_additive "Elements of an add right cancel semigroup are add-right-regular"]
 lemma is_right_regular_of_right_cancel_semigroup [right_cancel_semigroup R] (g : R) :
   is_right_regular g :=
 mul_left_injective g
@@ -298,6 +336,8 @@ section cancel_monoid
 variables [cancel_monoid 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."]
 lemma is_regular_of_cancel_monoid (g : R) : is_regular g :=
 ⟨mul_right_injective g, mul_left_injective g⟩
 
diff --git a/src/group_theory/group_action/opposite.lean b/src/group_theory/group_action/opposite.lean
index ab6b833f3560e..10bdc5494a0fd 100644
--- a/src/group_theory/group_action/opposite.lean
+++ b/src/group_theory/group_action/opposite.lean
@@ -85,7 +85,8 @@ See also `monoid.to_opposite_mul_action` and `monoid_with_zero.to_opposite_mul_a
   a • a' = a' * a.unop := rfl
 
 /-- The right regular action of a group on itself is transitive. -/
-@[to_additive] instance mul_action.opposite_regular.is_pretransitive {G : Type*} [group G] :
+@[to_additive "The right regular action of an additive group on itself is transitive."]
+instance mul_action.opposite_regular.is_pretransitive {G : Type*} [group G] :
   mul_action.is_pretransitive Gᵐᵒᵖ G :=
 ⟨λ x y, ⟨op (x⁻¹ * y), mul_inv_cancel_left _ _⟩⟩