diff --git a/src/algebra/char_p/invertible.lean b/src/algebra/char_p/invertible.lean
index b4b3addf3f301..e54ec5996ea8b 100644
--- a/src/algebra/char_p/invertible.lean
+++ b/src/algebra/char_p/invertible.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import algebra.invertible
-import algebra.field
+import algebra.field.basic
 import algebra.char_p.basic
 
 /-!
diff --git a/src/algebra/continued_fractions/basic.lean b/src/algebra/continued_fractions/basic.lean
index 88d96c8fb994e..039949eb00e07 100644
--- a/src/algebra/continued_fractions/basic.lean
+++ b/src/algebra/continued_fractions/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 -/
 import data.seq.seq
-import algebra.field
+import algebra.field.basic
 /-!
 # Basic Definitions/Theorems for Continued Fractions
 
diff --git a/src/algebra/euclidean_domain.lean b/src/algebra/euclidean_domain.lean
index b0956ac2bd787..2c620dc21a53a 100644
--- a/src/algebra/euclidean_domain.lean
+++ b/src/algebra/euclidean_domain.lean
@@ -5,7 +5,7 @@ Authors: Louis Carlin, Mario Carneiro
 -/
 
 import data.int.basic
-import algebra.field
+import algebra.field.basic
 
 /-!
 # Euclidean domains
diff --git a/src/algebra/field.lean b/src/algebra/field/basic.lean
similarity index 100%
rename from src/algebra/field.lean
rename to src/algebra/field/basic.lean
diff --git a/src/algebra/field/opposite.lean b/src/algebra/field/opposite.lean
new file mode 100644
index 0000000000000..70012ffcdda94
--- /dev/null
+++ b/src/algebra/field/opposite.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+import algebra.field.basic
+import algebra.opposites
+
+/-!
+# Field structure on the multiplicative opposite
+-/
+
+variables (α : Type*)
+
+namespace mul_opposite
+
+instance [division_ring α] : division_ring αᵐᵒᵖ :=
+{ .. mul_opposite.group_with_zero α, .. mul_opposite.ring α }
+
+instance [field α] : field αᵐᵒᵖ :=
+{ .. mul_opposite.division_ring α, .. mul_opposite.comm_ring α }
+
+end mul_opposite
diff --git a/src/algebra/module/opposites.lean b/src/algebra/module/opposites.lean
index 382dc105b81f2..b527c86de9ff6 100644
--- a/src/algebra/module/opposites.lean
+++ b/src/algebra/module/opposites.lean
@@ -3,14 +3,14 @@ Copyright (c) 2020 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import algebra.opposites
+import group_theory.group_action.opposite
 import data.equiv.module
 
 /-!
 # Module operations on `Mᵐᵒᵖ`
 
-This file contains definitions that could not be placed into `algebra.opposites` due to import
-cycles.
+This file contains definitions that build on top of the group action definitions in
+`group_theory.group_action.opposite`.
 -/
 
 namespace mul_opposite
diff --git a/src/algebra/opposites.lean b/src/algebra/opposites.lean
index 17c5ebb41a6c2..2a0d0cec40f6b 100644
--- a/src/algebra/opposites.lean
+++ b/src/algebra/opposites.lean
@@ -3,15 +3,14 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import algebra.field
 import algebra.group.commute
-import group_theory.group_action.defs
+import algebra.ring.basic
 import data.equiv.mul_add
 
 /-!
 # Multiplicative opposite and algebraic operations on it
 
-In this file we define `mul_oppposite α = αᵐᵒᵖ` to be the multiplicative opposite of `α`. It
+In this file we define `mul_opposite α = αᵐᵒᵖ` to be the multiplicative opposite of `α`. It
 inherits all additive algebraic structures on `α`, and reverses the order of multipliers in
 multiplicative structures, i.e., `op (x * y) = op x * op y`, where `mul_opposite.op` is the
 canonical map from `α` to `αᵐᵒᵖ`.
@@ -294,89 +293,6 @@ instance [group_with_zero α] : group_with_zero αᵐᵒᵖ :=
   .. mul_opposite.monoid_with_zero α, .. mul_opposite.div_inv_monoid α,
   .. mul_opposite.nontrivial α }
 
-instance [division_ring α] : division_ring αᵐᵒᵖ :=
-{ .. mul_opposite.group_with_zero α, .. mul_opposite.ring α }
-
-instance [field α] : field αᵐᵒᵖ :=
-{ .. mul_opposite.division_ring α, .. mul_opposite.comm_ring α }
-
-instance (R : Type*) [monoid R] [mul_action R α] : mul_action R αᵐᵒᵖ :=
-{ one_smul := λ x, unop_injective $ one_smul R (unop x),
-  mul_smul := λ r₁ r₂ x, unop_injective $ mul_smul r₁ r₂ (unop x),
-  .. mul_opposite.has_scalar α R }
-
-instance (R : Type*) [monoid R] [add_monoid α] [distrib_mul_action R α] :
-  distrib_mul_action R αᵐᵒᵖ :=
-{ smul_add := λ r x₁ x₂, unop_injective $ smul_add r (unop x₁) (unop x₂),
-  smul_zero := λ r, unop_injective $ smul_zero r,
-  .. mul_opposite.mul_action α R }
-
-instance (R : Type*) [monoid R] [monoid α] [mul_distrib_mul_action R α] :
-  mul_distrib_mul_action R αᵐᵒᵖ :=
-{ smul_mul := λ r x₁ x₂, unop_injective $ smul_mul' r (unop x₂) (unop x₁),
-  smul_one := λ r, unop_injective $ smul_one r,
-  .. mul_opposite.mul_action α R }
-
-instance {M N} [has_scalar M N] [has_scalar M α] [has_scalar N α] [is_scalar_tower M N α] :
-  is_scalar_tower M N αᵐᵒᵖ :=
-⟨λ x y z, unop_injective $ smul_assoc _ _ _⟩
-
-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 _ _ _⟩
-
-/-- Like `has_mul.to_has_scalar`, but multiplies on the right.
-
-See also `monoid.to_opposite_mul_action` and `monoid_with_zero.to_opposite_mul_action`. -/
-instance _root_.has_mul.to_has_opposite_scalar [has_mul α] : has_scalar αᵐᵒᵖ α :=
-{ smul := λ c x, x * c.unop }
-
-@[simp] lemma op_smul_eq_mul [has_mul α] {a a' : α} : op a • a' = a' * a := rfl
-
--- TODO: add an additive version once we have additive opposites
-/-- The right regular action of a group on itself is transitive. -/
-instance _root_.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 _ _⟩⟩
-
-instance _root_.semigroup.opposite_smul_comm_class [semigroup α] :
-  smul_comm_class αᵐᵒᵖ α α :=
-{ smul_comm := λ x y z, (mul_assoc _ _ _) }
-
-instance _root_.semigroup.opposite_smul_comm_class' [semigroup α] :
-  smul_comm_class α αᵐᵒᵖ α :=
-{ smul_comm := λ x y z, (mul_assoc _ _ _).symm }
-
-/-- Like `monoid.to_mul_action`, but multiplies on the right. -/
-instance _root_.monoid.to_opposite_mul_action [monoid α] : mul_action αᵐᵒᵖ α :=
-{ smul := (•),
-  one_smul := mul_one,
-  mul_smul := λ x y r, (mul_assoc _ _ _).symm }
-
-instance _root_.is_scalar_tower.opposite_mid {M N} [monoid N] [has_scalar M N]
-  [smul_comm_class M N N] :
-  is_scalar_tower M Nᵐᵒᵖ N :=
-⟨λ x y z, mul_smul_comm _ _ _⟩
-
-instance _root_.smul_comm_class.opposite_mid {M N} [monoid N] [has_scalar M N]
-  [is_scalar_tower M N N] :
-  smul_comm_class M Nᵐᵒᵖ N :=
-⟨λ x y z, by { induction y using mul_opposite.rec, simp [smul_mul_assoc] }⟩
-
--- The above instance does not create an unwanted diamond, the two paths to
--- `mul_action αᵐᵒᵖ αᵐᵒᵖ` are defeq.
-example [monoid α] : monoid.to_mul_action αᵐᵒᵖ = mul_opposite.mul_action α αᵐᵒᵖ := rfl
-
-/-- `monoid.to_opposite_mul_action` is faithful on cancellative monoids. -/
-instance _root_.left_cancel_monoid.to_has_faithful_opposite_scalar [left_cancel_monoid α] :
-  has_faithful_scalar αᵐᵒᵖ α :=
-⟨λ x y h, unop_injective $ mul_left_cancel (h 1)⟩
-
-/-- `monoid.to_opposite_mul_action` is faithful on nontrivial cancellative monoids with zero. -/
-instance _root_.cancel_monoid_with_zero.to_has_faithful_opposite_scalar
-  [cancel_monoid_with_zero α] [nontrivial α] : has_faithful_scalar αᵐᵒᵖ α :=
-⟨λ x y h, unop_injective $ mul_left_cancel₀ one_ne_zero (h 1)⟩
-
 variable {α}
 
 lemma semiconj_by.op [has_mul α] {a x y : α} (h : semiconj_by a x y) :
diff --git a/src/algebra/order/field.lean b/src/algebra/order/field.lean
index 1b3766df2847d..96edaf4f9390e 100644
--- a/src/algebra/order/field.lean
+++ b/src/algebra/order/field.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
 -/
-import algebra.field
+import algebra.field.basic
 import algebra.group_power.order
 import algebra.order.ring
 import tactic.monotonicity.basic
diff --git a/src/algebra/periodic.lean b/src/algebra/periodic.lean
index 8ecdb85ec8979..fbe3a7f0da990 100644
--- a/src/algebra/periodic.lean
+++ b/src/algebra/periodic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Benjamin Davidson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Benjamin Davidson
 -/
+import algebra.field.opposite
 import algebra.module.basic
 import algebra.order.archimedean
 import data.int.parity
diff --git a/src/algebra/smul_with_zero.lean b/src/algebra/smul_with_zero.lean
index c390c5a97c492..3fc994aeee791 100644
--- a/src/algebra/smul_with_zero.lean
+++ b/src/algebra/smul_with_zero.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import algebra.group_power.basic
-import algebra.opposites
+import group_theory.group_action.opposite
 
 /-!
 # Introduce `smul_with_zero`
diff --git a/src/algebra/star/basic.lean b/src/algebra/star/basic.lean
index cbda1dfc407d5..a03be3eff4362 100644
--- a/src/algebra/star/basic.lean
+++ b/src/algebra/star/basic.lean
@@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import tactic.apply_fun
+import algebra.field.opposite
 import algebra.field_power
 import data.equiv.ring_aut
 import group_theory.group_action.units
+import group_theory.group_action.opposite
 import algebra.ring.comp_typeclasses
 
 /-!
diff --git a/src/data/equiv/ring.lean b/src/data/equiv/ring.lean
index 45c9edec7fc2a..09e68052dfb9a 100644
--- a/src/data/equiv/ring.lean
+++ b/src/data/equiv/ring.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
 import data.equiv.mul_add
-import algebra.field
+import algebra.field.basic
 import algebra.opposites
 import algebra.big_operators.basic
 
diff --git a/src/data/equiv/transfer_instance.lean b/src/data/equiv/transfer_instance.lean
index 88b000a26b3e3..9841ced5485a0 100644
--- a/src/data/equiv/transfer_instance.lean
+++ b/src/data/equiv/transfer_instance.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import algebra.algebra.basic
-import algebra.field
+import algebra.field.basic
 import algebra.group.type_tags
 import ring_theory.ideal.local_ring
 import data.equiv.basic
diff --git a/src/group_theory/group_action/opposite.lean b/src/group_theory/group_action/opposite.lean
new file mode 100644
index 0000000000000..bd546f3b9f491
--- /dev/null
+++ b/src/group_theory/group_action/opposite.lean
@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2020 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import algebra.opposites
+import group_theory.group_action.defs
+
+/-!
+# Scalar actions on and by `Mᵐᵒᵖ`
+
+This file defines the actions on the opposite type `has_scalar R Mᵐᵒᵖ`, and actions by the opposite
+type, `has_scalar Rᵐᵒᵖ M`.
+
+Note that `mul_opposite.has_scalar` is provided in an earlier file as it is needed to provide the
+`add_monoid.nsmul` and `add_comm_group.gsmul` fields.
+-/
+
+variables (α : Type*)
+
+/-! ### Actions _on_ the opposite type
+
+Actions on the opposite type just act on the underlying type.
+-/
+
+namespace mul_opposite
+
+instance (R : Type*) [monoid R] [mul_action R α] : mul_action R αᵐᵒᵖ :=
+{ one_smul := λ x, unop_injective $ one_smul R (unop x),
+  mul_smul := λ r₁ r₂ x, unop_injective $ mul_smul r₁ r₂ (unop x),
+  .. mul_opposite.has_scalar α R }
+
+instance (R : Type*) [monoid R] [add_monoid α] [distrib_mul_action R α] :
+  distrib_mul_action R αᵐᵒᵖ :=
+{ smul_add := λ r x₁ x₂, unop_injective $ smul_add r (unop x₁) (unop x₂),
+  smul_zero := λ r, unop_injective $ smul_zero r,
+  .. mul_opposite.mul_action α R }
+
+instance (R : Type*) [monoid R] [monoid α] [mul_distrib_mul_action R α] :
+  mul_distrib_mul_action R αᵐᵒᵖ :=
+{ smul_mul := λ r x₁ x₂, unop_injective $ smul_mul' r (unop x₂) (unop x₁),
+  smul_one := λ r, unop_injective $ smul_one r,
+  .. mul_opposite.mul_action α R }
+
+instance {M N} [has_scalar M N] [has_scalar M α] [has_scalar N α] [is_scalar_tower M N α] :
+  is_scalar_tower M N αᵐᵒᵖ :=
+⟨λ x y z, unop_injective $ smul_assoc _ _ _⟩
+
+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 _ _ _⟩
+
+end mul_opposite
+
+/-! ### Actions _by_ the opposite type (right actions)
+
+In `has_mul.to_has_scalar` in another file, we define the left action `a₁ • a₂ = a₁ * a₂`. For the
+multiplicative opposite, we define `mul_opposite.op a₁ • a₂ = a₂ * a₁`, with the multiplication
+reversed.
+-/
+
+open mul_opposite
+
+/-- Like `has_mul.to_has_scalar`, but multiplies on the right.
+
+See also `monoid.to_opposite_mul_action` and `monoid_with_zero.to_opposite_mul_action_with_zero`. -/
+instance has_mul.to_has_opposite_scalar [has_mul α] : has_scalar αᵐᵒᵖ α :=
+{ smul := λ c x, x * c.unop }
+
+@[simp] lemma op_smul_eq_mul [has_mul α] {a a' : α} : op a • a' = a' * a := rfl
+
+-- TODO: add an additive version once we have additive opposites
+/-- The right regular action of a 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 _ _⟩⟩
+
+instance semigroup.opposite_smul_comm_class [semigroup α] :
+  smul_comm_class αᵐᵒᵖ α α :=
+{ smul_comm := λ x y z, (mul_assoc _ _ _) }
+
+instance semigroup.opposite_smul_comm_class' [semigroup α] :
+  smul_comm_class α αᵐᵒᵖ α :=
+{ smul_comm := λ x y z, (mul_assoc _ _ _).symm }
+
+/-- Like `monoid.to_mul_action`, but multiplies on the right. -/
+instance monoid.to_opposite_mul_action [monoid α] : mul_action αᵐᵒᵖ α :=
+{ smul := (•),
+  one_smul := mul_one,
+  mul_smul := λ x y r, (mul_assoc _ _ _).symm }
+
+instance is_scalar_tower.opposite_mid {M N} [monoid N] [has_scalar M N]
+  [smul_comm_class M N N] :
+  is_scalar_tower M Nᵐᵒᵖ N :=
+⟨λ x y z, mul_smul_comm _ _ _⟩
+
+instance smul_comm_class.opposite_mid {M N} [monoid N] [has_scalar M N]
+  [is_scalar_tower M N N] :
+  smul_comm_class M Nᵐᵒᵖ N :=
+⟨λ x y z, by { induction y using mul_opposite.rec, simp [smul_mul_assoc] }⟩
+
+-- The above instance does not create an unwanted diamond, the two paths to
+-- `mul_action αᵐᵒᵖ αᵐᵒᵖ` are defeq.
+example [monoid α] : monoid.to_mul_action αᵐᵒᵖ = mul_opposite.mul_action α αᵐᵒᵖ := rfl
+
+/-- `monoid.to_opposite_mul_action` is faithful on cancellative monoids. -/
+instance left_cancel_monoid.to_has_faithful_opposite_scalar [left_cancel_monoid α] :
+  has_faithful_scalar αᵐᵒᵖ α :=
+⟨λ x y h, unop_injective $ mul_left_cancel (h 1)⟩
+
+/-- `monoid.to_opposite_mul_action` is faithful on nontrivial cancellative monoids with zero. -/
+instance cancel_monoid_with_zero.to_has_faithful_opposite_scalar
+  [cancel_monoid_with_zero α] [nontrivial α] : has_faithful_scalar αᵐᵒᵖ α :=
+⟨λ x y h, unop_injective $ mul_left_cancel₀ one_ne_zero (h 1)⟩
diff --git a/src/group_theory/group_action/prod.lean b/src/group_theory/group_action/prod.lean
index b51322ab9e2f1..2646bcfa45d4f 100644
--- a/src/group_theory/group_action/prod.lean
+++ b/src/group_theory/group_action/prod.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Eric Wieser
 -/
 import algebra.group.prod
+import group_theory.group_action.defs
 
 /-!
 # Prod instances for additive and multiplicative actions
diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean
index 23efc1e7ead18..f0925155ba792 100644
--- a/src/group_theory/submonoid/operations.lean
+++ b/src/group_theory/submonoid/operations.lean
@@ -9,6 +9,7 @@ import group_theory.submonoid.basic
 import data.equiv.mul_add
 import algebra.group.prod
 import algebra.group.inj_surj
+import group_theory.group_action.defs
 
 /-!
 # Operations on `submonoid`s
diff --git a/src/number_theory/number_field.lean b/src/number_theory/number_field.lean
index f860448765d65..57e99fd73d094 100644
--- a/src/number_theory/number_field.lean
+++ b/src/number_theory/number_field.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ashvni Narayanan, Anne Baanen
 -/
 
-import algebra.field
+import algebra.field.basic
 import data.rat.basic
 import ring_theory.algebraic
 import ring_theory.dedekind_domain
diff --git a/src/number_theory/pythagorean_triples.lean b/src/number_theory/pythagorean_triples.lean
index 4611650d5ebbf..5a23e00571e35 100644
--- a/src/number_theory/pythagorean_triples.lean
+++ b/src/number_theory/pythagorean_triples.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Paul van Wamelen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul van Wamelen
 -/
-import algebra.field
+import algebra.field.basic
 import ring_theory.int.basic
 import algebra.group_with_zero.power
 import tactic.ring