feat(dynamics/periodic_pts): Iteration is injective below the period (#…

…13660)

This PR adds `iterate_injective_of_lt_minimal_period`, generalizing `pow_injective_of_lt_order_of`.

src/dynamics/periodic_pts.lean

@@ -237,6 +237,9 @@ begin
   { exact is_periodic_pt_zero f x }
 end
 
+lemma iterate_minimal_period (f : α → α) (x : α) : f^[minimal_period f x] x = x :=
+is_periodic_pt_minimal_period f x
+
 lemma iterate_eq_mod_minimal_period : f^[n] x = (f^[n % minimal_period f x] x) :=
 ((is_periodic_pt_minimal_period f x).iterate_mod_apply n).symm
 
@@ -261,6 +264,16 @@ begin
   exact nat.find_min' (mk_mem_periodic_pts hn hx) ⟨hn, hx⟩
 end
 
+lemma iterate_injective_of_lt_minimal_period (hm : m < minimal_period f x)
+  (hn : n < minimal_period f x) (hf : (f^[m] x) = (f^[n] x)) : m = n :=
+begin
+  wlog h_le : n ≤ m,
+  rw [←h_le.le_iff_eq, ←tsub_le_tsub_iff_left hm.le, tsub_le_iff_right],
+  apply is_periodic_pt.minimal_period_le (nat.add_pos_left (tsub_pos_of_lt hm) n),
+  rw [is_periodic_pt, is_fixed_pt, iterate_add_apply, ←hf, ←iterate_add_apply,
+      nat.sub_add_cancel hm.le, iterate_minimal_period],
+end
+
 lemma minimal_period_id : minimal_period id x = 1 :=
 ((is_periodic_id _ _ ).minimal_period_le nat.one_pos).antisymm
   (nat.succ_le_of_lt ((is_periodic_id _ _ ).minimal_period_pos nat.one_pos))

src/group_theory/order_of_element.lean

@@ -317,25 +317,10 @@ end monoid_add_monoid
 section cancel_monoid
 variables [left_cancel_monoid G] (x y)
 
-@[to_additive]
-lemma pow_injective_aux (h : n ≤ m)
-  (hm : m < order_of x) (eq : x ^ n = x ^ m) : n = m :=
-by_contradiction $ assume ne : n ≠ m,
-  have h₁ : m - n > 0, from nat.pos_of_ne_zero (by simp [tsub_eq_iff_eq_add_of_le h, ne.symm]),
-  have h₂ : m = n + (m - n) := (add_tsub_cancel_of_le h).symm,
-  have h₃ : x ^ (m - n) = 1,
-    by { rw [h₂, pow_add] at eq, apply mul_left_cancel, convert eq.symm, exact mul_one (x ^ n) },
-  have le : order_of x ≤ m - n, from order_of_le_of_pow_eq_one h₁ h₃,
-  have lt : m - n < order_of x,
-    from (tsub_lt_iff_left h).mpr $ nat.lt_add_left _ _ _ hm,
-  lt_irrefl _ (le.trans_lt lt)
-
 @[to_additive nsmul_injective_of_lt_add_order_of]
 lemma pow_injective_of_lt_order_of
   (hn : n < order_of x) (hm : m < order_of x) (eq : x ^ n = x ^ m) : n = m :=
-(le_total n m).elim
-  (assume h, pow_injective_aux x h hm eq)
-  (assume h, (pow_injective_aux x h hn eq.symm).symm)
+iterate_injective_of_lt_minimal_period hn hm (by simpa only [mul_left_iterate, mul_one])
 
 @[to_additive mem_multiples_iff_mem_range_add_order_of']
 lemma mem_powers_iff_mem_range_order_of' [decidable_eq G] (hx : 0 < order_of x) :