feat(algebra/group_with_zero/power): With zero lemmas (#11051)

This proves the `group_with_zero` variant of some lemmas and moves lemmas from `algebra.group_power.basic` to `algebra.group_with_zero.power`.

Author: YaelDillies

src/algebra/group_power/basic.lean

@@ -17,6 +17,8 @@ which in turn depends on other parts of algebra.
 This module contains lemmas about `a ^ n` and `n • a`, where `n : ℕ` or `n : ℤ`.
 Further lemmas can be found in `algebra.group_power.lemmas`.
 
+The analogous results for groups with zero can be found in `algebra.group_with_zero.power`.
+
 ## Notation
 
 - `a ^ n` is used as notation for `has_pow.pow a n`; in this file `n : ℕ` or `n : ℤ`.

src/algebra/group_with_zero/power.lean

@@ -37,7 +37,7 @@ lemma ring.inverse_pow (r : M) : ∀ (n : ℕ), ring.inverse r ^ n = ring.invers
 end zero
 
 section group_with_zero
-variables {G₀ : Type*} [group_with_zero G₀]
+variables {G₀ : Type*} [group_with_zero G₀] {a : G₀} {m n : ℕ}
 
 section nat_pow
 
@@ -53,9 +53,22 @@ have h1 : m - n + n = m, from tsub_add_cancel_of_le h,
 have h2 : a ^ (m - n) * a ^ n = a ^ m, by rw [←pow_add, h1],
 by simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2
 
+lemma pow_sub_of_lt (a : G₀) {m n : ℕ} (h : n < m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
+begin
+  obtain rfl | ha := eq_or_ne a 0,
+  { rw [zero_pow (tsub_pos_of_lt h), zero_pow (n.zero_le.trans_lt h), zero_mul] },
+  { exact pow_sub₀ _ ha h.le }
+end
+
 theorem pow_inv_comm₀ (a : G₀) (m n : ℕ) : (a⁻¹) ^ m * a ^ n = a ^ n * (a⁻¹) ^ m :=
 (commute.refl a).inv_left₀.pow_pow m n
 
+lemma inv_pow_sub₀ (ha : a ≠ 0) (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n :=
+by rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow₀, inv_pow₀, inv_inv₀]
+
+lemma inv_pow_sub_of_lt (a : G₀) (h : n < m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n :=
+by rw [pow_sub_of_lt a⁻¹ h, inv_pow₀, inv_pow₀, inv_inv₀]
+
 end nat_pow
 
 end group_with_zero
@@ -74,7 +87,7 @@ lemma zero_zpow : ∀ z : ℤ, z ≠ 0 → (0 : G₀) ^ z = 0
 | (n : ℕ) h := by { rw [zpow_coe_nat, zero_pow'], simpa using h }
 | -[1+n]  h := by simp
 
-lemma fzero_pow_eq (n : ℤ) : (0 : G₀) ^ n = if n = 0 then 1 else 0 :=
+lemma zero_zpow_eq (n : ℤ) : (0 : G₀) ^ n = if n = 0 then 1 else 0 :=
 begin
   split_ifs with h,
   { rw [h, zpow_zero] },
@@ -86,6 +99,12 @@ end
 | 0       := by { change a ^ (0 : ℤ) = (a ^ (0 : ℤ))⁻¹, simp }
 | -[1+ n] := by { rw [zpow_neg_succ_of_nat, inv_inv₀, ← zpow_coe_nat], refl }
 
+lemma mul_zpow_neg_one₀ (a b : G₀) : (a * b) ^ (-1 : ℤ) = b ^ (-1 : ℤ) * a ^ (-1 : ℤ) :=
+by simp only [mul_inv_rev₀, zpow_one, zpow_neg₀]
+
+lemma zpow_neg_one₀ (x : G₀) : x ^ (-1 : ℤ) = x⁻¹ :=
+by { rw [← congr_arg has_inv.inv (pow_one x), zpow_neg₀, ← zpow_coe_nat], refl }
+
 theorem inv_zpow₀ (a : G₀) : ∀n:ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
 | (n : ℕ) := by rw [zpow_coe_nat, zpow_coe_nat, inv_pow₀]
 | -[1+ n] := by rw [zpow_neg_succ_of_nat, zpow_neg_succ_of_nat, inv_pow₀]
@@ -189,10 +208,6 @@ lemma commute.mul_zpow₀ {a b : G₀} (h : commute a b) :
 | (n : ℕ) := by simp [h.mul_pow n]
 | -[1+n]  := by simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev₀]
 
-lemma mul_zpow₀ {G₀ : Type*} [comm_group_with_zero G₀] (a b : G₀) (m : ℤ):
-  (a * b) ^ m = (a ^ m) * (b ^ m) :=
-(commute.all a b).mul_zpow₀ m
-
 theorem zpow_bit0' (a : G₀) (n : ℤ) : a ^ bit0 n = (a * a) ^ n :=
 (zpow_bit0₀ a n).trans ((commute.refl a).mul_zpow₀ n).symm
 
@@ -233,6 +248,9 @@ variables {G₀ : Type*} [comm_group_with_zero G₀]
   (a / b) ^ n = a ^ n / b ^ n :=
 by simp only [div_eq_mul_inv, mul_pow, inv_pow₀]
 
+lemma mul_zpow₀ (a b : G₀) (m : ℤ) : (a * b) ^ m = (a ^ m) * (b ^ m) :=
+(commute.all a b).mul_zpow₀ m
+
 @[simp] theorem div_zpow₀ (a : G₀) {b : G₀} (n : ℤ) :
   (a / b) ^ n = a ^ n / b ^ n :=
 by simp only [div_eq_mul_inv, mul_zpow₀, inv_zpow₀]
@@ -244,6 +262,13 @@ begin
   rw [sq, mul_assoc, mul_div_cancel_left _ ha]
 end
 
+/-- The `n`-th power map (`n` an integer) on a commutative group with zero, considered as a group
+homomorphism. -/
+def zpow_group_hom₀ (n : ℤ) : G₀ →* G₀ :=
+{ to_fun := (^ n),
+  map_one' := one_zpow₀ n,
+  map_mul' := λ a b, mul_zpow₀ a b n }
+
 end
 
 /-- If a monoid homomorphism `f` between two `group_with_zero`s maps `0` to `0`, then it maps `x^n`,