From e0c204ef90a47d38f2390667546ea8a89d773c35 Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Fri, 27 Sep 2019 20:10:21 +0200
Subject: [PATCH] chore(algebra/group_power): move inv_one from group_power to
 field (#1495)

* chore(algebra/group_power): move inv_one from group_power to field

*  fix
---
 src/algebra/field.lean       | 2 ++
 src/algebra/group_power.lean | 2 --
 2 files changed, 2 insertions(+), 2 deletions(-)

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