feat(algebra/group_power/basic): add lemmas about pow and neg on units (#11447)

In future we might want to add a typeclass for monoids with a well-behaved negation operator to avoid needing to repeat these lemmas. Such a typeclass would also apply to the `unitary` submonoid too.

Author: eric-wieser

src/algebra/group/units_hom.lean

@@ -43,6 +43,14 @@ variable {M}
 
 @[simp, to_additive] lemma coe_hom_apply (x : Mˣ) : coe_hom M x = ↑x := rfl
 
+@[simp, norm_cast, to_additive]
+lemma coe_pow (u : Mˣ) (n : ℕ) : ((u ^ n : Mˣ) : M) = u ^ n :=
+(units.coe_hom M).map_pow u n
+
+@[simp, norm_cast, to_additive]
+lemma coe_zpow {G} [group G] (u : Gˣ) (n : ℤ) : ((u ^ n : Gˣ) : G) = u ^ n :=
+(units.coe_hom G).map_zpow u n
+
 /-- If a map `g : M → Nˣ` agrees with a homomorphism `f : M →* N`, then
 this map is a monoid homomorphism too. -/
 @[to_additive "If a map `g : M → add_units N` agrees with a homomorphism `f : M →+ N`, then this map

src/algebra/group_power/basic.lean

@@ -381,6 +381,33 @@ by simp [sq]
 
 alias neg_sq ← neg_pow_two
 
+/- Copies of the above ring lemmas for `units R`. -/
+namespace units
+
+section
+variables (R)
+theorem neg_one_pow_eq_or : ∀ n : ℕ, (-1 : Rˣ)^n = 1 ∨ (-1 : Rˣ)^n = -1
+| 0     := or.inl (pow_zero _)
+| (n+1) := (neg_one_pow_eq_or n).swap.imp
+  (λ h, by rw [pow_succ, h, ←units.neg_eq_neg_one_mul, units.neg_neg])
+  (λ h, by rw [pow_succ, h, mul_one])
+
+end
+
+theorem neg_pow (a : Rˣ) (n : ℕ) : (- a) ^ n = (-1) ^ n * a ^ n :=
+(units.neg_eq_neg_one_mul a).symm ▸ (commute.units_neg_one_left a).mul_pow n
+
+@[simp] theorem neg_pow_bit0 (a : Rˣ) (n : ℕ) : (- a) ^ (bit0 n) = a ^ (bit0 n) :=
+by rw [pow_bit0', units.neg_mul_neg, pow_bit0']
+
+@[simp] theorem neg_pow_bit1 (a : Rˣ) (n : ℕ) : (- a) ^ (bit1 n) = - a ^ (bit1 n) :=
+by simp only [bit1, pow_succ, neg_pow_bit0, units.neg_mul_eq_neg_mul]
+
+@[simp] lemma neg_sq (a : Rˣ) : (-a)^2 = a^2 :=
+by simp [sq]
+
+end units
+
 end ring
 
 section comm_ring
@@ -400,6 +427,18 @@ by rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
 
 alias sub_sq ← sub_pow_two
 
+/- Copies of the above comm_ring lemmas for `units R`. -/
+namespace units
+
+lemma eq_or_eq_neg_of_sq_eq_sq [is_domain R] (a b : Rˣ) (h : a ^ 2 = b ^ 2) : a = b ∨ a = -b :=
+begin
+  refine (eq_or_eq_neg_of_sq_eq_sq _ _ _).imp (λ h, units.ext h) (λ h, units.ext h),
+  replace h := congr_arg (coe : Rˣ → R) h,
+  rwa [units.coe_pow, units.coe_pow] at h,
+end
+
+end units
+
 end comm_ring
 
 lemma of_add_nsmul [add_monoid A] (x : A) (n : ℕ) :

src/algebra/group_power/lemmas.lean

@@ -32,10 +32,6 @@ begin
   { simp }
 end
 
-@[simp, norm_cast, to_additive]
-lemma units.coe_pow (u : Mˣ) (n : ℕ) : ((u ^ n : Mˣ) : M) = u ^ n :=
-(units.coe_hom M).map_pow u n
-
 instance invertible_pow (m : M) [invertible m] (n : ℕ) : invertible (m ^ n) :=
 { inv_of := ⅟ m ^ n,
   inv_of_mul_self := by rw [← (commute_inv_of m).symm.mul_pow, inv_of_mul_self, one_pow],
@@ -171,10 +167,6 @@ theorem zpow_bit0 (a : G) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n := zpow_add _ _
 theorem zpow_bit1 (a : G) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a :=
 by rw [bit1, zpow_add, zpow_bit0, zpow_one]
 
-@[simp, norm_cast, to_additive]
-lemma units.coe_zpow (u : Gˣ) (n : ℤ) : ((u ^ n : Gˣ) : G) = u ^ n :=
-(units.coe_hom G).map_zpow u n
-
 end group
 
 section ordered_add_comm_group

src/algebra/ring/basic.lean

@@ -803,7 +803,15 @@ units.ext $ neg_mul _ _
 /-- Multiplication of elements of a ring's unit group commutes with mapping the second argument
     to its additive inverse. -/
 @[simp] protected theorem mul_neg (u₁ u₂ : αˣ) : u₁ * -u₂ = -(u₁ * u₂) :=
-units.ext $ (neg_mul_eq_mul_neg _ _).symm
+units.ext $ mul_neg _ _
+
+/-- `units` version of `neg_mul_eq_neg_mul`. -/
+lemma neg_mul_eq_neg_mul (a b : αˣ) : -(a * b) = -a * b :=
+units.ext $ neg_mul_eq_neg_mul _ _
+
+/-- `units` version of `neg_mul_eq_mul_neg`. -/
+lemma neg_mul_eq_mul_neg (a b : αˣ) : -(a * b) = a * -b :=
+units.ext $ neg_mul_eq_mul_neg _ _
 
 /-- Multiplication of the additive inverses of two elements of a ring's unit group equals
     multiplication of the two original elements. -/
@@ -813,6 +821,10 @@ units.ext $ (neg_mul_eq_mul_neg _ _).symm
     one times the original element. -/
 protected theorem neg_eq_neg_one_mul (u : αˣ) : -u = -1 * u := by simp
 
+lemma mul_neg_one (a : α) : a * -1 = -a := by simp
+
+lemma neg_one_mul (a : α) : -1 * a = -a := by simp
+
 end units
 
 lemma is_unit.neg [ring α] {a : α} : is_unit a → is_unit (-a)
@@ -1141,6 +1153,7 @@ by simp only [semiconj_by, left_distrib, right_distrib, h.eq, h'.eq]
   semiconj_by (a + b) x y :=
 by simp only [semiconj_by, left_distrib, right_distrib, ha.eq, hb.eq]
 
+section
 variables [ring R] {a b x y x' y' : R}
 
 lemma neg_right (h : semiconj_by a x y) : semiconj_by a (-x) (-y) :=
@@ -1169,6 +1182,32 @@ by simpa only [sub_eq_add_neg] using h.add_right h'.neg_right
   semiconj_by (a - b) x y :=
 by simpa only [sub_eq_add_neg] using ha.add_left hb.neg_left
 
+end
+
+/- Copies of the above ring lemmas for `units R`. -/
+section units
+variables [ring R] {a b x y x' y' : Rˣ}
+
+lemma units_neg_right (h : semiconj_by a x y) : semiconj_by a (-x) (-y) :=
+by simp only [semiconj_by, h.eq, units.neg_mul, units.mul_neg]
+
+@[simp] lemma units_neg_right_iff : semiconj_by a (-x) (-y) ↔ semiconj_by a x y :=
+⟨λ h, units.neg_neg x ▸ units.neg_neg y ▸ h.units_neg_right, semiconj_by.units_neg_right⟩
+
+lemma units_neg_left (h : semiconj_by a x y) : semiconj_by (-a) x y :=
+by simp only [semiconj_by, h.eq, units.neg_mul, units.mul_neg]
+
+@[simp] lemma units_neg_left_iff : semiconj_by (-a) x y ↔ semiconj_by a x y :=
+⟨λ h, units.neg_neg a ▸ h.units_neg_left, semiconj_by.units_neg_left⟩
+
+@[simp] lemma units_neg_one_right (a : Rˣ) : semiconj_by a (-1) (-1) :=
+(one_right a).units_neg_right
+
+@[simp] lemma units_neg_one_left (x : Rˣ) : semiconj_by (-1) x x :=
+(semiconj_by.one_left x).units_neg_left
+
+end units
+
 end semiconj_by
 
 namespace commute
@@ -1193,6 +1232,7 @@ h.bit0_right.add_right (commute.one_right x)
 lemma bit1_left [semiring R] {x y : R} (h : commute x y) : commute (bit1 x) y :=
 h.bit0_left.add_left (commute.one_left y)
 
+section
 variables [ring R] {a b c : R}
 
 theorem neg_right : commute a b → commute a (- b) := semiconj_by.neg_right
@@ -1207,4 +1247,22 @@ theorem neg_left : commute a b → commute (- a) b := semiconj_by.neg_left
 @[simp] theorem sub_right : commute a b → commute a c → commute a (b - c) := semiconj_by.sub_right
 @[simp] theorem sub_left : commute a c → commute b c → commute (a - b) c := semiconj_by.sub_left
 
+end
+
+/- Copies of the above ring lemmas for `units R`. -/
+section units
+variables [ring R] {a b c : Rˣ}
+
+theorem units_neg_right : commute a b → commute a (- b) := semiconj_by.units_neg_right
+@[simp] theorem units_neg_right_iff : commute a (-b) ↔ commute a b :=
+semiconj_by.units_neg_right_iff
+
+theorem units_neg_left : commute a b → commute (- a) b := semiconj_by.units_neg_left
+@[simp] theorem units_neg_left_iff : commute (-a) b ↔ commute a b := semiconj_by.units_neg_left_iff
+
+@[simp] theorem units_neg_one_right (a : Rˣ) : commute a (-1) := semiconj_by.units_neg_one_right a
+@[simp] theorem units_neg_one_left (a : Rˣ) : commute (-1) a := semiconj_by.units_neg_one_left a
+
+end units
+
 end commute