diff --git a/src/algebra/field.lean b/src/algebra/field.lean
index d2b4725ff0a1a..4a3e9d4703a39 100644
--- a/src/algebra/field.lean
+++ b/src/algebra/field.lean
@@ -19,6 +19,8 @@ instance division_ring.to_domain [s : division_ring α] : domain α :=
       division_ring.mul_ne_zero (mt or.inl hn) (mt or.inr hn) h
   ..s }
 
+@[simp] theorem inv_one [division_ring α] : (1⁻¹ : α) = 1 := by rw [inv_eq_one_div, one_div_one]
+
 @[simp] theorem inv_inv' [discrete_field α] (x : α) : x⁻¹⁻¹ = x :=
 if h : x = 0
 then by rw [h, inv_zero, inv_zero]
diff --git a/src/algebra/group_power.lean b/src/algebra/group_power.lean
index 70c8c96eee483..28c8eb798405b 100644
--- a/src/algebra/group_power.lean
+++ b/src/algebra/group_power.lean
@@ -17,8 +17,6 @@ import data.int.basic data.list.basic
 universes u v
 variable {α : Type u}
 
-@[simp] theorem inv_one [division_ring α] : (1⁻¹ : α) = 1 := by rw [inv_eq_one_div, one_div_one]
-
 /-- The power operation in a monoid. `a^n = a*a*...*a` n times. -/
 def monoid.pow [monoid α] (a : α) : ℕ → α
 | 0     := 1