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

@@ -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]

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