chore: Delete Algebra.GroupPower.Basic, Algebra.GroupWithZero.Bitwise (#11855)

The entire `Algebra.GroupPower` folder is problematic in that it treats `pow` as an advanced subject while the rest of mathlib wants to treat it as a primitive. As such, its existence is an obstacle to developing the theory of `pow` transversally.

This PR scatters the lemmas in `Algebra.GroupPower.Basic` to earlier files and deletes it. Also delete `Algebra.GroupWithZero.Bitwise` whose lemmas are completely deprecated (and hard to rehome).

See #9411 for previous work.

Author: YaelDillies

Mathlib.lean

@@ -248,7 +248,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.Identities
 import Mathlib.Algebra.GroupPower.IterateHom
@@ -258,7 +257,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/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

@@ -3,10 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
-import Mathlib.Algebra.Field.Defs
-import Mathlib.Algebra.GroupWithZero.Commute
-import Mathlib.Algebra.GroupWithZero.Bitwise
-import Mathlib.Algebra.Ring.Parity
+import Mathlib.Data.Int.Parity
 
 #align_import algebra.field.power from "leanprover-community/mathlib"@"1e05171a5e8cf18d98d9cf7b207540acb044acae"
 
@@ -25,15 +22,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]

Mathlib/Algebra/Group/Basic.lean

@@ -678,6 +678,13 @@ lemma zpow_mul' (a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m := by rw [Int.m
 #align zpow_mul' zpow_mul'
 #align mul_zsmul mul_zsmul
 
+#noalign zpow_bit0
+#noalign bit0_zsmul
+#noalign zpow_bit0'
+#noalign bit0_zsmul'
+#noalign zpow_bit1
+#noalign bit1_zsmul
+
 variable (a b c)
 
 @[to_additive, field_simps] -- The attributes are out of order on purpose

Mathlib/Algebra/Group/Commute/Basic.lean

@@ -99,5 +99,44 @@ protected theorem conj_iff (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹) 
 protected theorem conj (comm : Commute a b) (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹) :=
   (Commute.conj_iff h).mpr comm
 
+@[to_additive (attr := simp)]
+lemma zpow_right (h : Commute a b) (m : ℤ) : Commute a (b ^ m) := SemiconjBy.zpow_right h m
+#align commute.zpow_right Commute.zpow_right
+#align add_commute.zsmul_right AddCommute.zsmul_right
+
+@[to_additive (attr := simp)]
+lemma zpow_left (h : Commute a b) (m : ℤ) : Commute (a ^ m) b := (h.symm.zpow_right m).symm
+#align commute.zpow_left Commute.zpow_left
+#align add_commute.zsmul_left AddCommute.zsmul_left
+
+@[to_additive] lemma zpow_zpow (h : Commute a b) (m n : ℤ) : Commute (a ^ m) (b ^ n) :=
+  (h.zpow_left m).zpow_right n
+#align commute.zpow_zpow Commute.zpow_zpow
+#align add_commute.zsmul_zsmul AddCommute.zsmul_zsmul
+
+variable (a) (m n : ℤ)
+
+@[to_additive] lemma self_zpow : Commute a (a ^ n) := (Commute.refl a).zpow_right n
+#align commute.self_zpow Commute.self_zpow
+#align add_commute.self_zsmul AddCommute.self_zsmul
+
+@[to_additive] lemma zpow_self : Commute (a ^ n) a := (Commute.refl a).zpow_left n
+#align commute.zpow_self Commute.zpow_self
+#align add_commute.zsmul_self AddCommute.zsmul_self
+
+@[to_additive] lemma zpow_zpow_self : Commute (a ^ m) (a ^ n) := (Commute.refl a).zpow_zpow m n
+#align commute.zpow_zpow_self Commute.zpow_zpow_self
+#align add_commute.zsmul_zsmul_self AddCommute.zsmul_zsmul_self
+
 end Group
 end Commute
+
+section Group
+variable [Group G]
+
+@[to_additive] lemma pow_inv_comm (a : G) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m :=
+  (Commute.refl a).inv_left.pow_pow _ _
+#align pow_inv_comm pow_inv_comm
+#align nsmul_neg_comm nsmul_neg_comm
+
+end Group

Mathlib/Algebra/Group/Commute/Defs.lean

@@ -28,11 +28,11 @@ Most of the proofs come from the properties of `SemiconjBy`.
 -/
 
 
-variable {G : Type*}
+variable {G M S : Type*}
 
 /-- Two elements commute if `a * b = b * a`. -/
 @[to_additive "Two elements additively commute if `a + b = b + a`"]
-def Commute {S : Type*} [Mul S] (a b : S) : Prop :=
+def Commute [Mul S] (a b : S) : Prop :=
   SemiconjBy a b b
 #align commute Commute
 #align add_commute AddCommute
@@ -41,13 +41,13 @@ def Commute {S : Type*} [Mul S] (a b : S) : Prop :=
 Two elements `a` and `b` commute if `a * b = b * a`.
 -/
 @[to_additive]
-theorem commute_iff_eq {S : Type*} [Mul S] (a b : S) : Commute a b ↔ a * b = b * a := Iff.rfl
+theorem commute_iff_eq [Mul S] (a b : S) : Commute a b ↔ a * b = b * a := Iff.rfl
 
 namespace Commute
 
 section Mul
 
-variable {S : Type*} [Mul S]
+variable [Mul S]
 
 /-- Equality behind `Commute a b`; useful for rewriting. -/
 @[to_additive "Equality behind `AddCommute a b`; useful for rewriting."]
@@ -97,7 +97,7 @@ end Mul
 
 section Semigroup
 
-variable {S : Type*} [Semigroup S] {a b c : S}
+variable [Semigroup S] {a b c : S}
 
 /-- If `a` commutes with both `b` and `c`, then it commutes with their product. -/
 @[to_additive (attr := simp)
@@ -140,15 +140,15 @@ protected theorem mul_mul_mul_comm (hbc : Commute b c) (a d : S) :
 end Semigroup
 
 @[to_additive]
-protected theorem all {S : Type*} [CommMagma S] (a b : S) : Commute a b :=
+protected theorem all [CommMagma S] (a b : S) : Commute a b :=
   mul_comm a b
 #align commute.all Commute.allₓ
 #align add_commute.all AddCommute.allₓ
 -- not sure why this needs an `ₓ`, maybe instance names not aligned?
 
 section MulOneClass
 
-variable {M : Type*} [MulOneClass M]
+variable [MulOneClass M]
 
 @[to_additive (attr := simp)]
 theorem one_right (a : M) : Commute a 1 :=
@@ -168,7 +168,7 @@ end MulOneClass
 
 section Monoid
 
-variable {M : Type*} [Monoid M] {a b : M}
+variable [Monoid M] {a b : M}
 
 @[to_additive (attr := simp)]
 theorem pow_right (h : Commute a b) (n : ℕ) : Commute a (b ^ n) :=
@@ -216,6 +216,11 @@ theorem pow_pow_self (a : M) (m n : ℕ) : Commute (a ^ m) (a ^ n) :=
 #align add_commute.nsmul_nsmul_self AddCommute.nsmul_nsmul_selfₓ
 -- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
 
+@[to_additive] lemma mul_pow (h : Commute a b) : ∀ n, (a * b) ^ n = a ^ n * b ^ n
+  | 0 => by rw [pow_zero, pow_zero, pow_zero, one_mul]
+  | n + 1 => by simp only [pow_succ', h.mul_pow n, ← mul_assoc, (h.pow_left n).right_comm]
+#align commute.mul_pow Commute.mul_pow
+
 end Monoid
 
 section DivisionMonoid
@@ -232,6 +237,13 @@ protected theorem inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
 #align commute.inv Commute.inv
 #align add_commute.neg AddCommute.neg
 
+@[to_additive AddCommute.zsmul_add]
+protected lemma mul_zpow (h : Commute a b) : ∀ n : ℤ, (a * b) ^ n = a ^ n * b ^ n
+  | (n : ℕ)    => by simp [zpow_natCast, h.mul_pow n]
+  | .negSucc n => by simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]
+#align commute.mul_zpow Commute.mul_zpow
+#align add_commute.zsmul_add AddCommute.zsmul_add
+
 end DivisionMonoid
 
 section Group
@@ -253,3 +265,31 @@ theorem mul_inv_cancel_assoc (h : Commute a b) : a * (b * a⁻¹) = b := by
 end Group
 
 end Commute
+
+set_option linter.deprecated false
+
+section Monoid
+variable [Monoid M]
+
+@[to_additive bit0_nsmul]
+lemma pow_bit0 (a : M) (n : ℕ) : a ^ bit0 n = a ^ n * a ^ n := pow_add _ _ _
+#align pow_bit0 pow_bit0
+#align bit0_nsmul bit0_nsmul
+
+@[to_additive bit1_nsmul]
+lemma pow_bit1 (a : M) (n : ℕ) : a ^ bit1 n = a ^ n * a ^ n * a := by rw [bit1, pow_succ, pow_bit0]
+#align pow_bit1 pow_bit1
+#align bit1_nsmul bit1_nsmul
+
+@[to_additive bit0_nsmul']
+lemma pow_bit0' (a : M) (n : ℕ) : a ^ bit0 n = (a * a) ^ n := by
+  rw [pow_bit0, (Commute.refl a).mul_pow]
+#align pow_bit0' pow_bit0'
+#align bit0_nsmul' bit0_nsmul'
+
+@[to_additive bit1_nsmul']
+lemma pow_bit1' (a : M) (n : ℕ) : a ^ bit1 n = (a * a) ^ n * a := by rw [bit1, pow_succ, pow_bit0']
+#align pow_bit1' pow_bit1'
+#align bit1_nsmul' bit1_nsmul'
+
+end Monoid

Mathlib/Algebra/Group/Defs.lean

@@ -582,10 +582,6 @@ monoids. To work, it has to map fields to fields. This means that we should also
 fields to the multiplicative structure `Monoid`, which could solve defeq problems for powers if
 needed. These problems do not come up in practice, so most of the time we will not need to adjust
 the `npow` field when defining multiplicative objects.
-
-A basic theory for the power function on monoids and the `ℕ`-action on additive monoids is built in
-the file `Algebra.GroupPower.Basic`. For now, we only register the most basic properties that we
-need right away.
 -/
 
 

Mathlib/Algebra/Group/Even.lean

@@ -31,9 +31,7 @@ This file defines square and even elements in a monoid.
 `Mathlib.Algebra.Ring.Parity` for the definition of odd elements.
 -/
 
--- TODO: After #11855
--- assert_not_exists MonoidWithZero
-assert_not_exists Ring
+assert_not_exists MonoidWithZero
 
 open MulOpposite
 

Mathlib/Algebra/Group/Hom/End.lean

@@ -59,9 +59,9 @@ end AddMonoid.End
 /-!
 ### Miscellaneous definitions
 
-Due to the fact this file imports `Algebra.GroupPower.Basic`, it is not possible to import it in
-some of the lower-level files like `Algebra.Ring.Basic`. The following lemmas should be rehomed
-if the import structure permits them to be.
+This file used to import `Algebra.GroupPower.Basic`, hence it was not possible to import it in
+some of the lower-level files like `Algebra.Ring.Basic`. The following lemmas should be rehomed now
+that `Algebra.GroupPower.Basic` was deleted.
 -/
 
 

Mathlib/Algebra/Group/Int.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad
 -/
 import Mathlib.Algebra.Group.Nat
 import Mathlib.Order.Monotone.Basic
+import Mathlib.Tactic.Common
 
 #align_import data.int.basic from "leanprover-community/mathlib"@"00d163e35035c3577c1c79fa53b68de17781ffc1"
 #align_import data.int.units from "leanprover-community/mathlib"@"641b6a82006416ec431b2987b354af9311fed4f2"