diff --git a/src/algebra/module/hom.lean b/src/algebra/module/hom.lean
index 3b3a7d881cf7f..232b20064ec51 100644
--- a/src/algebra/module/hom.lean
+++ b/src/algebra/module/hom.lean
@@ -41,6 +41,9 @@ instance [smul_comm_class R S B] : smul_comm_class R S (A →+ B) :=
 instance [has_scalar R S] [is_scalar_tower R S B] : is_scalar_tower R S (A →+ B) :=
 ⟨λ a b f, ext $ λ x, smul_assoc _ _ _⟩
 
+instance [distrib_mul_action Rᵐᵒᵖ B] [is_central_scalar R B] : is_central_scalar R (A →+ B) :=
+⟨λ a b, ext $ λ x, op_smul_eq_smul _ _⟩
+
 end
 
 instance [semiring R] [add_monoid A] [add_comm_monoid B] [module R B] :
diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean
index c858a5bf7f571..7f55b65ff28a7 100644
--- a/src/algebra/module/linear_map.lean
+++ b/src/algebra/module/linear_map.lean
@@ -635,6 +635,10 @@ instance [smul_comm_class S T M₂] : smul_comm_class S T (M →ₛₗ[σ₁₂]
 instance [has_scalar S T] [is_scalar_tower S T M₂] : is_scalar_tower S T (M →ₛₗ[σ₁₂] M₂) :=
 { smul_assoc := λ _ _ _, ext $ λ _, smul_assoc _ _ _ }
 
+instance [distrib_mul_action Sᵐᵒᵖ M₂] [smul_comm_class R₂ Sᵐᵒᵖ M₂] [is_central_scalar S M₂] :
+  is_central_scalar S (M →ₛₗ[σ₁₂] M₂) :=
+{ op_smul_eq_smul := λ a b, ext $ λ x, op_smul_eq_smul _ _ }
+
 instance : distrib_mul_action S (M →ₛₗ[σ₁₂] M₂) :=
 { one_smul := λ f, ext $ λ _, one_smul _ _,
   mul_smul := λ c c' f, ext $ λ _, mul_smul _ _ _,
diff --git a/src/algebra/module/submodule_pointwise.lean b/src/algebra/module/submodule_pointwise.lean
index 8655ebcfac52d..b42fc22198edb 100644
--- a/src/algebra/module/submodule_pointwise.lean
+++ b/src/algebra/module/submodule_pointwise.lean
@@ -68,6 +68,11 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submodule R M) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
 
+instance pointwise_central_scalar [distrib_mul_action αᵐᵒᵖ M] [smul_comm_class αᵐᵒᵖ R M]
+  [is_central_scalar α M] :
+  is_central_scalar α (submodule R M) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ linear_map.ext $ by exact op_smul_eq_smul _⟩
+
 @[simp] lemma smul_le_self_of_tower {α : Type*}
   [semiring α] [module α R] [module α M] [smul_comm_class α R M] [is_scalar_tower α R M]
   (a : α) (S : submodule R M) : a • S ≤ S :=
diff --git a/src/algebra/module/ulift.lean b/src/algebra/module/ulift.lean
index 011a90f343dfa..df0e18071df94 100644
--- a/src/algebra/module/ulift.lean
+++ b/src/algebra/module/ulift.lean
@@ -46,6 +46,10 @@ instance is_scalar_tower'' [has_scalar R M] [has_scalar M N] [has_scalar R N]
   [is_scalar_tower R M N] : is_scalar_tower R M (ulift N) :=
 ⟨λ x y z, show up ((x • y) • z.down) = ⟨x • y • z.down⟩, by rw smul_assoc⟩
 
+instance [has_scalar R M] [has_scalar Rᵐᵒᵖ M] [is_central_scalar R M] :
+  is_central_scalar R (ulift M) :=
+⟨λ r m, congr_arg up $ op_smul_eq_smul r m.down⟩
+
 instance mul_action [monoid R] [mul_action R M] :
   mul_action (ulift R) M :=
 { smul := (•),
diff --git a/src/algebra/monoid_algebra/basic.lean b/src/algebra/monoid_algebra/basic.lean
index b33553e67080b..5b35c7982685c 100644
--- a/src/algebra/monoid_algebra/basic.lean
+++ b/src/algebra/monoid_algebra/basic.lean
@@ -257,6 +257,11 @@ instance [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mu
   smul_comm_class R S (monoid_algebra k G) :=
 finsupp.smul_comm_class G k
 
+instance [monoid R] [semiring k] [distrib_mul_action R k] [distrib_mul_action Rᵐᵒᵖ k]
+  [is_central_scalar R k] :
+  is_central_scalar R (monoid_algebra k G) :=
+finsupp.is_central_scalar G k
+
 instance comap_distrib_mul_action_self [group G] [semiring k] :
   distrib_mul_action G (monoid_algebra k G) :=
 finsupp.comap_distrib_mul_action_self
@@ -984,6 +989,11 @@ instance [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mu
   smul_comm_class R S (add_monoid_algebra k G) :=
 finsupp.smul_comm_class G k
 
+instance [monoid R] [semiring k] [distrib_mul_action R k] [distrib_mul_action Rᵐᵒᵖ k]
+  [is_central_scalar R k] :
+  is_central_scalar R (add_monoid_algebra k G) :=
+finsupp.is_central_scalar G k
+
 /-! It is hard to state the equivalent of `distrib_mul_action G (add_monoid_algebra k G)`
 because we've never discussed actions of additive groups. -/
 
diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean
index 2679c1fe68fcf..882c3ec6ff5b4 100644
--- a/src/algebra/pointwise.lean
+++ b/src/algebra/pointwise.lean
@@ -564,6 +564,10 @@ instance is_scalar_tower'' {γ : Type*}
   is_scalar_tower (set α) (set β) (set γ) :=
 { smul_assoc := λ T T' T'', image2_assoc smul_assoc }
 
+instance is_central_scalar [has_scalar α β] [has_scalar αᵐᵒᵖ β] [is_central_scalar α β] :
+  is_central_scalar α (set β) :=
+⟨λ a S, congr_arg (λ f, f '' S) $ by exact funext (λ _, op_smul_eq_smul _ _)⟩
+
 section monoid
 
 /-! ### `set α` as a `(∪,*)`-semiring -/
diff --git a/src/data/complex/module.lean b/src/data/complex/module.lean
index 81ea489f3e542..138f931f48c9c 100644
--- a/src/data/complex/module.lean
+++ b/src/data/complex/module.lean
@@ -62,6 +62,10 @@ instance [has_scalar R S] [has_scalar R ℝ] [has_scalar S ℝ] [is_scalar_tower
   is_scalar_tower R S ℂ :=
 { smul_assoc := λ r s x, by ext; simp [smul_re, smul_im, smul_assoc] }
 
+instance [has_scalar R ℝ] [has_scalar Rᵐᵒᵖ ℝ] [is_central_scalar R ℝ] :
+  is_central_scalar R ℂ :=
+{ op_smul_eq_smul := λ r x, by ext; simp [smul_re, smul_im, op_smul_eq_smul] }
+
 instance [monoid R] [mul_action R ℝ] : mul_action R ℂ :=
 { one_smul := λ x, by ext; simp [smul_re, smul_im, one_smul],
   mul_smul := λ r s x, by ext; simp [smul_re, smul_im, mul_smul] }
diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean
index fc51219560ed9..b5243ecc93a75 100644
--- a/src/data/dfinsupp.lean
+++ b/src/data/dfinsupp.lean
@@ -254,6 +254,11 @@ instance {δ : Type*} [monoid γ] [monoid δ]
   is_scalar_tower γ δ (Π₀ i, β i) :=
 { smul_assoc := λ r s m, ext $ λ i, by simp only [smul_apply, smul_assoc r s (m i)] }
 
+instance [monoid γ] [Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)]
+  [Π i, distrib_mul_action γᵐᵒᵖ (β i)] [∀ i, is_central_scalar γ (β i)] :
+  is_central_scalar γ (Π₀ i, β i) :=
+{ op_smul_eq_smul := λ r m, ext $ λ i, by simp only [smul_apply, op_smul_eq_smul r (m i)] }
+
 /-- Dependent functions with finite support inherit a `distrib_mul_action` structure from such a
 structure on each coordinate. -/
 instance [monoid γ] [Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)] :
diff --git a/src/data/finsupp/basic.lean b/src/data/finsupp/basic.lean
index 8f068f33162cf..ded49c42b7668 100644
--- a/src/data/finsupp/basic.lean
+++ b/src/data/finsupp/basic.lean
@@ -2300,6 +2300,10 @@ instance [monoid R] [monoid S] [add_monoid M] [distrib_mul_action R M] [distrib_
   smul_comm_class R S (α →₀ M) :=
 { smul_comm := λ r s a, ext $ λ _, smul_comm _ _ _ }
 
+instance [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M]
+  [is_central_scalar R M] : is_central_scalar R (α →₀ M) :=
+{ op_smul_eq_smul := λ r a, ext $ λ _, op_smul_eq_smul _ _ }
+
 instance [semiring R] [add_comm_monoid M] [module R M] : module R (α →₀ M) :=
 { smul      := (•),
   zero_smul := λ x, ext $ λ _, zero_smul _ _,
diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean
index 5b4138a8c6084..a724c6a961079 100644
--- a/src/data/matrix/basic.lean
+++ b/src/data/matrix/basic.lean
@@ -117,6 +117,8 @@ instance [has_scalar R α] [has_scalar S α] [smul_comm_class R S α] :
   smul_comm_class R S (matrix m n α) := pi.smul_comm_class
 instance [has_scalar R S] [has_scalar R α] [has_scalar S α] [is_scalar_tower R S α] :
   is_scalar_tower R S (matrix m n α) := pi.is_scalar_tower
+instance [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α] :
+  is_central_scalar R (matrix m n α) := pi.is_central_scalar
 instance [monoid R] [mul_action R α] :
   mul_action R (matrix m n α) := pi.mul_action _
 instance [monoid R] [add_monoid α] [distrib_mul_action R α] :
diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean
index 58013e58f6d30..e04f28885991b 100644
--- a/src/data/mv_polynomial/basic.lean
+++ b/src/data/mv_polynomial/basic.lean
@@ -119,6 +119,10 @@ instance [monoid R] [monoid S₁][comm_semiring S₂]
   [distrib_mul_action R S₂] [distrib_mul_action S₁ S₂] [smul_comm_class R S₁ S₂] :
   smul_comm_class R S₁ (mv_polynomial σ S₂) :=
 add_monoid_algebra.smul_comm_class
+instance [monoid R] [comm_semiring S₁] [distrib_mul_action R S₁] [distrib_mul_action Rᵐᵒᵖ S₁]
+  [is_central_scalar R S₁] :
+  is_central_scalar R (mv_polynomial σ S₁) :=
+add_monoid_algebra.is_central_scalar
 instance [comm_semiring R] [comm_semiring S₁] [algebra R S₁] : algebra R (mv_polynomial σ S₁) :=
 add_monoid_algebra.algebra
 -- TODO[gh-6025]: make this an instance once safe to do so
diff --git a/src/data/polynomial/basic.lean b/src/data/polynomial/basic.lean
index a0db56a375830..9b52fca766f97 100644
--- a/src/data/polynomial/basic.lean
+++ b/src/data/polynomial/basic.lean
@@ -150,6 +150,10 @@ instance {S₁ S₂} [has_scalar S₁ S₂] [monoid S₁] [monoid S₂] [distrib
   [distrib_mul_action S₂ R] [is_scalar_tower S₁ S₂ R] : is_scalar_tower S₁ S₂ (polynomial R) :=
 ⟨by { rintros _ _ ⟨⟩, simp [smul_to_finsupp] }⟩
 
+instance {S} [monoid S] [distrib_mul_action S R] [distrib_mul_action Sᵐᵒᵖ R]
+  [is_central_scalar S R] : is_central_scalar S (polynomial R) :=
+⟨by { rintros _ ⟨⟩, simp [smul_to_finsupp, op_smul_eq_smul] }⟩
+
 instance [subsingleton R] : unique (polynomial R) :=
 { uniq := by { rintros ⟨x⟩, change (⟨x⟩ : polynomial R) = 0, rw [← zero_to_finsupp], simp },
 .. polynomial.inhabited }
diff --git a/src/group_theory/group_action/defs.lean b/src/group_theory/group_action/defs.lean
index aebe56b0ad852..e35ec6e1cd106 100644
--- a/src/group_theory/group_action/defs.lean
+++ b/src/group_theory/group_action/defs.lean
@@ -6,6 +6,7 @@ Authors: Chris Hughes, Yury Kudryashov
 import algebra.group.defs
 import algebra.group.hom
 import algebra.group.type_tags
+import algebra.opposites
 import logic.embedding
 
 /-!
@@ -27,6 +28,7 @@ interaction of different group actions,
 
 * `smul_comm_class M N α` and its additive version `vadd_comm_class M N α`;
 * `is_scalar_tower M N α` (no additive version).
+* `is_central_scalar M α` (no additive version).
 
 ## Notation
 
@@ -181,6 +183,18 @@ is_scalar_tower.smul_assoc x y z
 
 instance semigroup.is_scalar_tower [semigroup α] : is_scalar_tower α α α := ⟨mul_assoc⟩
 
+/-- A typeclass indicating that the right (aka `mul_opposite`) and left actions by `M` on `α` are
+equal, that is that `M` acts centrally on `α`. This can be thought of as a version of commutativity
+for `•`. -/
+class is_central_scalar (M α : Type*) [has_scalar M α] [has_scalar Mᵐᵒᵖ α] : Prop :=
+(op_smul_eq_smul : ∀ (m : M) (a : α), mul_opposite.op m • a = m • a)
+
+lemma is_central_scalar.unop_smul_eq_smul {M α : Type*} [has_scalar M α] [has_scalar Mᵐᵒᵖ α]
+  [is_central_scalar M α] (m : Mᵐᵒᵖ) (a : α) : (mul_opposite.unop m) • a = m • a :=
+mul_opposite.rec (by exact λ m, (is_central_scalar.op_smul_eq_smul _ _).symm) m
+
+export is_central_scalar (op_smul_eq_smul unop_smul_eq_smul)
+
 namespace has_scalar
 variables [has_scalar M α]
 
diff --git a/src/group_theory/group_action/opposite.lean b/src/group_theory/group_action/opposite.lean
index 8cf08ac3f4de9..e9fe58fcceff2 100644
--- a/src/group_theory/group_action/opposite.lean
+++ b/src/group_theory/group_action/opposite.lean
@@ -50,6 +50,18 @@ instance {M N} [has_scalar M α] [has_scalar N α] [smul_comm_class M N α] :
   smul_comm_class M N αᵐᵒᵖ :=
 ⟨λ x y z, unop_injective $ smul_comm _ _ _⟩
 
+instance (R : Type*) [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α] :
+  is_central_scalar R αᵐᵒᵖ :=
+⟨λ r m, unop_injective $ op_smul_eq_smul _ _⟩
+
+lemma op_smul_eq_op_smul_op {R : Type*} [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α]
+  (r : R) (a : α) : op (r • a) = op r • op a :=
+(op_smul_eq_smul r (op a)).symm
+
+lemma unop_smul_eq_unop_smul_unop {R : Type*} [has_scalar R α] [has_scalar Rᵐᵒᵖ α]
+  [is_central_scalar R α] (r : Rᵐᵒᵖ) (a : αᵐᵒᵖ) : unop (r • a) = unop r • unop a :=
+(unop_smul_eq_smul r (unop a)).symm
+
 end mul_opposite
 
 /-! ### Actions _by_ the opposite type (right actions)
@@ -83,6 +95,9 @@ instance semigroup.opposite_smul_comm_class' [semigroup α] :
   smul_comm_class α αᵐᵒᵖ α :=
 { smul_comm := λ x y z, (mul_assoc _ _ _).symm }
 
+instance comm_semigroup.is_central_scalar [comm_semigroup α] : is_central_scalar α α :=
+⟨λ r m, mul_comm _ _⟩
+
 /-- Like `monoid.to_mul_action`, but multiplies on the right. -/
 instance monoid.to_opposite_mul_action [monoid α] : mul_action αᵐᵒᵖ α :=
 { smul := (•),
diff --git a/src/group_theory/group_action/pi.lean b/src/group_theory/group_action/pi.lean
index 87cd25e479502..afae7ce4c1bc2 100644
--- a/src/group_theory/group_action/pi.lean
+++ b/src/group_theory/group_action/pi.lean
@@ -71,6 +71,10 @@ instance smul_comm_class'' {g : I → Type*} {h : I → Type*}
   [∀ i, smul_comm_class (f i) (g i) (h i)] : smul_comm_class (Π i, f i) (Π i, g i) (Π i, h i) :=
 ⟨λ x y z, funext $ λ i, smul_comm (x i) (y i) (z i)⟩
 
+instance {α : Type*} [Π i, has_scalar α $ f i] [Π i, has_scalar αᵐᵒᵖ $ f i]
+  [∀ i, is_central_scalar α (f i)] : is_central_scalar α (Π i, f i) :=
+⟨λ r m, funext $ λ i, op_smul_eq_smul _ _⟩
+
 /-- If `f i` has a faithful scalar action for a given `i`, then so does `Π i, f i`. This is
 not an instance as `i` cannot be inferred. -/
 @[to_additive pi.has_faithful_vadd_at]
diff --git a/src/group_theory/group_action/prod.lean b/src/group_theory/group_action/prod.lean
index 2646bcfa45d4f..69387d74bb25f 100644
--- a/src/group_theory/group_action/prod.lean
+++ b/src/group_theory/group_action/prod.lean
@@ -35,6 +35,10 @@ instance [has_scalar M N] [is_scalar_tower M N α] [is_scalar_tower M N β] :
   smul_comm_class M N (α × β) :=
 { smul_comm := λ r s x, mk.inj_iff.mpr ⟨smul_comm _ _ _, smul_comm _ _ _⟩ }
 
+instance [has_scalar Mᵐᵒᵖ α] [has_scalar Mᵐᵒᵖ β] [is_central_scalar M α] [is_central_scalar M β] :
+  is_central_scalar M (α × β) :=
+⟨λ r m, prod.ext (op_smul_eq_smul _ _) (op_smul_eq_smul _ _)⟩
+
 @[to_additive has_faithful_vadd_left]
 instance has_faithful_scalar_left [has_faithful_scalar M α] [nonempty β] :
   has_faithful_scalar M (α × β) :=
diff --git a/src/group_theory/subgroup/pointwise.lean b/src/group_theory/subgroup/pointwise.lean
index 2af228cc40da5..315a3e8ff6bdb 100644
--- a/src/group_theory/subgroup/pointwise.lean
+++ b/src/group_theory/subgroup/pointwise.lean
@@ -53,6 +53,10 @@ lemma pointwise_smul_def {a : α} (S : subgroup G) :
 lemma smul_mem_pointwise_smul (m : G) (a : α) (S : subgroup G) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set G))
 
+instance pointwise_central_scalar [mul_distrib_mul_action αᵐᵒᵖ G] [is_central_scalar α G] :
+  is_central_scalar α (subgroup G) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ monoid_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group
@@ -143,6 +147,10 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_subgroup A) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
 
+instance pointwise_central_scalar [distrib_mul_action αᵐᵒᵖ A] [is_central_scalar α A] :
+  is_central_scalar α (add_subgroup A) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ add_monoid_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group
diff --git a/src/group_theory/submonoid/pointwise.lean b/src/group_theory/submonoid/pointwise.lean
index ee3334906fdba..7817f0d4fdc4e 100644
--- a/src/group_theory/submonoid/pointwise.lean
+++ b/src/group_theory/submonoid/pointwise.lean
@@ -130,6 +130,10 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submonoid M) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
 
+instance pointwise_central_scalar [mul_distrib_mul_action αᵐᵒᵖ M] [is_central_scalar α M] :
+  is_central_scalar α (submonoid M) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ monoid_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group
@@ -220,6 +224,10 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_submonoid A) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
 
+instance pointwise_central_scalar [distrib_mul_action αᵐᵒᵖ A] [is_central_scalar α A] :
+  is_central_scalar α (add_submonoid A) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ add_monoid_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group
diff --git a/src/ring_theory/subring/pointwise.lean b/src/ring_theory/subring/pointwise.lean
index 9a8c773a797d7..8b31487e935ea 100644
--- a/src/ring_theory/subring/pointwise.lean
+++ b/src/ring_theory/subring/pointwise.lean
@@ -55,6 +55,10 @@ lemma pointwise_smul_def {a : M} (S : subring R) :
 lemma smul_mem_pointwise_smul (m : M) (r : R) (S : subring R) : r ∈ S → m • r ∈ m • S :=
 (set.smul_mem_smul_set : _ → _ ∈ m • (S : set R))
 
+instance pointwise_central_scalar [mul_semiring_action Mᵐᵒᵖ R] [is_central_scalar M R] :
+  is_central_scalar M (subring R) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ ring_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 
diff --git a/src/ring_theory/subsemiring/pointwise.lean b/src/ring_theory/subsemiring/pointwise.lean
index c624e49ffede2..347f66d6f1c2b 100644
--- a/src/ring_theory/subsemiring/pointwise.lean
+++ b/src/ring_theory/subsemiring/pointwise.lean
@@ -51,6 +51,10 @@ lemma pointwise_smul_def {a : M} (S : subsemiring R) :
 lemma smul_mem_pointwise_smul (m : M) (r : R) (S : subsemiring R) : r ∈ S → m • r ∈ m • S :=
 (set.smul_mem_smul_set : _ → _ ∈ m • (S : set R))
 
+instance pointwise_central_scalar [mul_semiring_action Mᵐᵒᵖ R] [is_central_scalar M R] :
+  is_central_scalar M (subsemiring R) :=
+⟨λ a S, congr_arg (λ f, S.map f) $ ring_hom.ext $ by exact op_smul_eq_smul _⟩
+
 end monoid
 
 section group