[Merged by Bors] - chore: Delete Algebra.GroupPower.Basic, Algebra.GroupWithZero.Bitwise

Mathlib.lean

@@ -244,7 +244,6 @@ import Mathlib.Algebra.Group.Units.Equiv
 import Mathlib.Algebra.Group.Units.Hom
 import Mathlib.Algebra.Group.WithOne.Basic
 import Mathlib.Algebra.Group.WithOne.Defs
-import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.GroupPower.CovariantClass
 import Mathlib.Algebra.GroupPower.Hom
 import Mathlib.Algebra.GroupPower.Identities
@@ -256,7 +255,6 @@ import Mathlib.Algebra.GroupRingAction.Basic
 import Mathlib.Algebra.GroupRingAction.Invariant
 import Mathlib.Algebra.GroupRingAction.Subobjects
 import Mathlib.Algebra.GroupWithZero.Basic
-import Mathlib.Algebra.GroupWithZero.Bitwise
 import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.GroupWithZero.Divisibility

Mathlib/Algebra/BigOperators/List/Lemmas.lean

@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 import Mathlib.Algebra.BigOperators.List.Basic
 import Mathlib.Algebra.Group.Opposite
-import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Ring.Basic

Mathlib/Algebra/Divisibility/Basic.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
 Neil Strickland, Aaron Anderson
 -/
-import Mathlib.Algebra.GroupPower.Basic
+import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Tactic.Common
 
 #align_import algebra.divisibility.basic from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 

Mathlib/Algebra/Divisibility/Prod.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Prod
+import Mathlib.Tactic.Common
 
 /-!
 # Lemmas about the divisibility relation in product (semi)groups

Mathlib/Algebra/Field/Power.lean

@@ -5,8 +5,8 @@ Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.GroupWithZero.Power
-import Mathlib.Algebra.GroupWithZero.Bitwise
 import Mathlib.Algebra.Parity
+import Mathlib.Data.Int.Parity
 
 #align_import algebra.field.power from "leanprover-community/mathlib"@"1e05171a5e8cf18d98d9cf7b207540acb044acae"
 
@@ -25,15 +25,11 @@ section DivisionRing
 
 variable [DivisionRing α] {n : ℤ}
 
-set_option linter.deprecated false in
-@[simp]
-theorem zpow_bit1_neg (a : α) (n : ℤ) : (-a) ^ bit1 n = -a ^ bit1 n := by
-  rw [zpow_bit1', zpow_bit1', neg_mul_neg, neg_mul_eq_mul_neg]
-#align zpow_bit1_neg zpow_bit1_neg
-
 theorem Odd.neg_zpow (h : Odd n) (a : α) : (-a) ^ n = -a ^ n := by
-  obtain ⟨k, rfl⟩ := h.exists_bit1
-  exact zpow_bit1_neg _ _
+  have hn : n ≠ 0 := by rintro rfl; exact Int.odd_iff_not_even.1 h even_zero
+  obtain ⟨k, rfl⟩ := h
+  simp_rw [zpow_add' (.inr (.inl hn)), zpow_one, zpow_mul, zpow_two, neg_mul_neg,
+    neg_mul_eq_mul_neg]
 #align odd.neg_zpow Odd.neg_zpow
 
 theorem Odd.neg_one_zpow (h : Odd n) : (-1 : α) ^ n = -1 := by rw [h.neg_zpow, one_zpow]