fix(algebra/group_power): put opposite lemmas in the right namespace (#…

…8100)

src/algebra/geom_sum.lean

@@ -75,7 +75,7 @@ by { have : 1 - 1 - 0 = 0 := rfl,
 @[simp] lemma op_geom_sum₂ [ring α] (x y : α) (n : ℕ) :
   op (geom_sum₂ x y n) = geom_sum₂ (op y) (op x) n :=
 begin
-  simp only [geom_sum₂_def, op_sum, op_mul, units.op_pow],
+  simp only [geom_sum₂_def, op_sum, op_mul, op_pow],
   rw ← sum_range_reflect,
   refine sum_congr rfl (λ j j_in, _),
   rw [mem_range, nat.lt_iff_add_one_le] at j_in,
@@ -151,7 +151,7 @@ lemma commute.mul_neg_geom_sum₂ [ring α] {x y : α} (h : commute x y) (n : 
   (y - x) * (geom_sum₂ x y n) = y ^ n - x ^ n :=
 begin
   rw ← op_inj_iff,
-  simp only [op_mul, op_sub, op_geom_sum₂, units.op_pow],
+  simp only [op_mul, op_sub, op_geom_sum₂, op_pow],
   exact (commute.op h.symm).geom_sum₂_mul n
 end
 
@@ -255,7 +255,7 @@ protected theorem commute.geom_sum₂_Ico_mul [ring α] {x y : α} (h : commute
   (∑ i in finset.Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n -  y ^ (n - m) * x ^ m :=
 begin
   rw ← op_inj_iff,
-  simp only [op_sub, op_mul, units.op_pow, op_sum],
+  simp only [op_sub, op_mul, op_pow, op_sum],
   have : ∑ k in Ico m n, op y ^ (n - 1 - k) * op x ^ k
     = ∑ k in Ico m n, op x ^ k * op y ^ (n - 1 - k),
   { refine sum_congr rfl (λ k k_in, _),

src/algebra/group_power/lemmas.lean

@@ -820,8 +820,10 @@ lemma conj_pow (u : units M) (x : M) (n : ℕ) : (↑u * x * ↑(u⁻¹))^n = u
 lemma conj_pow' (u : units M) (x : M) (n : ℕ) : (↑(u⁻¹) * x * u)^n = ↑(u⁻¹) * x^n * u:=
 (u⁻¹).conj_pow x n
 
-open opposite
+end units
 
+namespace opposite
+variables [monoid M]
 /-- Moving to the opposite monoid commutes with taking powers. -/
 @[simp] lemma op_pow (x : M) (n : ℕ) : op (x ^ n) = (op x) ^ n :=
 begin
@@ -837,4 +839,4 @@ begin
   { rw [pow_succ', unop_mul, h, pow_succ] }
 end
 
-end units
+end opposite