feat(group_theory/order_of_element): generalised to add_order_of (#6770)

This PR defines `add_order_of` for an additive monoid. If someone sees how to do this with more automation, let me know. 

This gets one step towards closing issue #1563.

Coauthored by: Yakov Pechersky @pechersky 



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>

src/algebra/group/type_tags.lean

@@ -129,12 +129,18 @@ instance [has_one α] : has_zero (additive α) := ⟨additive.of_mul 1⟩
 
 @[simp] lemma of_mul_one [has_one α] : @additive.of_mul α 1 = 0 := rfl
 
+@[simp] lemma of_mul_eq_zero {A : Type*} [has_one A] {x : A} :
+  additive.of_mul x = 0 ↔ x = 1 := iff.rfl
+
 @[simp] lemma to_mul_zero [has_one α] : (0 : additive α).to_mul = 1 := rfl
 
 instance [has_zero α] : has_one (multiplicative α) := ⟨multiplicative.of_add 0⟩
 
 @[simp] lemma of_add_zero [has_zero α] : @multiplicative.of_add α 0 = 1 := rfl
 
+@[simp] lemma of_add_eq_one {A : Type*} [has_zero A] {x : A} :
+  multiplicative.of_add x = 1 ↔ x = 0 := iff.rfl
+
 @[simp] lemma to_add_one [has_zero α] : (1 : multiplicative α).to_add = 0 := rfl
 
 instance [monoid α] : add_monoid (additive α) :=
@@ -149,6 +155,18 @@ instance [add_monoid α] : monoid (multiplicative α) :=
   mul_one := @add_zero _ _,
   ..multiplicative.semigroup }
 
+instance [left_cancel_monoid α] : add_left_cancel_monoid (additive α) :=
+{ .. additive.add_monoid, .. additive.add_left_cancel_semigroup }
+
+instance [add_left_cancel_monoid α] : left_cancel_monoid (multiplicative α) :=
+{ .. multiplicative.monoid, .. multiplicative.left_cancel_semigroup }
+
+instance [right_cancel_monoid α] : add_right_cancel_monoid (additive α) :=
+{ .. additive.add_monoid, .. additive.add_right_cancel_semigroup }
+
+instance [add_right_cancel_monoid α] : right_cancel_monoid (multiplicative α) :=
+{ .. multiplicative.monoid, .. multiplicative.right_cancel_semigroup }
+
 instance [comm_monoid α] : add_comm_monoid (additive α) :=
 { .. additive.add_monoid, .. additive.add_comm_semigroup }
 

src/algebra/group_power/basic.lean

@@ -733,6 +733,13 @@ lemma of_add_nsmul [add_monoid A] (x : A) (n : ℕ) :
 lemma of_add_gsmul [add_group A] (x : A) (n : ℤ) :
   multiplicative.of_add (n •ℤ x) = (multiplicative.of_add x)^n := rfl
 
+lemma of_mul_pow {A : Type*} [monoid A] (x : A) (n : ℕ) :
+  additive.of_mul (x ^ n) = n •ℕ (additive.of_mul x) :=
+(congr_arg additive.of_mul (of_add_nsmul (additive.of_mul x) n)).symm
+
+lemma of_mul_gpow [group G] (x : G) (n : ℤ) : additive.of_mul (x ^ n) = n •ℤ additive.of_mul x :=
+by { cases n; simp [gsmul_of_nat, gpow_of_nat, of_mul_pow] }
+
 @[simp] lemma semiconj_by.gpow_right [group G] {a x y : G} (h : semiconj_by a x y) :
   ∀ m : ℤ, semiconj_by a (x^m) (y^m)
 | (n : ℕ) := h.pow_right n

src/data/equiv/basic.lean

@@ -343,6 +343,15 @@ by rw [set.image_subset_iff, e.image_eq_preimage]
 @[simp] lemma symm_image_image {α β} (e : α ≃ β) (s : set α) : e.symm '' (e '' s) = s :=
 by { rw [← set.image_comp], simp }
 
+lemma eq_image_iff_symm_image_eq {α β} (e : α ≃ β) (s : set α) (t : set β) :
+  t = e '' s ↔ e.symm '' t = s :=
+begin
+  refine (injective.eq_iff' _ _).symm,
+  { rw set.image_injective,
+    exact (equiv.symm e).injective },
+  { exact equiv.symm_image_image _ _ }
+end
+
 @[simp] lemma image_symm_image {α β} (e : α ≃ β) (s : set β) : e '' (e.symm '' s) = s :=
 e.symm.symm_image_image s
 

src/data/int/gcd.lean

@@ -347,3 +347,11 @@ begin
   rw [← units.coe_one, ← gpow_coe_nat, ← units.ext_iff] at *,
   simp only [nat.gcd_eq_gcd_ab, gpow_add, gpow_mul, hm, hn, one_gpow, one_mul]
 end
+
+lemma gcd_nsmul_eq_zero {M : Type*} [add_monoid M] (x : M) {m n : ℕ} (hm : m •ℕ x = 0)
+  (hn : n •ℕ x = 0) : (m.gcd n) •ℕ x = 0 :=
+begin
+  apply multiplicative.of_add.injective,
+  rw [of_add_nsmul, of_add_zero, pow_gcd_eq_one];
+  rwa [←of_add_nsmul, ←of_add_zero, equiv.apply_eq_iff_eq]
+end