From d839ff4a5d3357058d15dc4ab398095635b2549a Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 14 Oct 2024 12:17:41 +0000
Subject: [PATCH] feat(OrderOfElement): add `isOfFinOrder_pow` (#17636)

Also add `IsOfFinOrder.of_pow` and a missing `@[to_additive]`.
---
 Mathlib/GroupTheory/OrderOfElement.lean | 26 ++++++++++++++++++++-----
 Mathlib/GroupTheory/Torsion.lean        |  2 +-
 2 files changed, 22 insertions(+), 6 deletions(-)

diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
index 9e33d48b21996..1d4e34b53c52d 100644
--- a/Mathlib/GroupTheory/OrderOfElement.lean
+++ b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -80,11 +80,32 @@ theorem not_isOfFinOrder_of_injective_pow {x : G} (h : Injective fun n : ℕ =>
   rw [h hnx] at hn_pos
   exact irrefl 0 hn_pos
 
+/-- 1 is of finite order in any monoid. -/
+@[to_additive (attr := simp) "0 is of finite order in any additive monoid."]
+theorem IsOfFinOrder.one : IsOfFinOrder (1 : G) :=
+  isOfFinOrder_iff_pow_eq_one.mpr ⟨1, Nat.one_pos, one_pow 1⟩
+
+@[to_additive (attr := deprecated (since := "2024-10-11"))]
+alias isOfFinOrder_one := IsOfFinOrder.one
+
+@[to_additive]
 lemma IsOfFinOrder.pow {n : ℕ} : IsOfFinOrder a → IsOfFinOrder (a ^ n) := by
   simp_rw [isOfFinOrder_iff_pow_eq_one]
   rintro ⟨m, hm, ha⟩
   exact ⟨m, hm, by simp [pow_right_comm _ n, ha]⟩
 
+@[to_additive]
+lemma IsOfFinOrder.of_pow {n : ℕ} (h : IsOfFinOrder (a ^ n)) (hn : n ≠ 0) : IsOfFinOrder a := by
+  rw [isOfFinOrder_iff_pow_eq_one] at *
+  rcases h with ⟨m, hm, ha⟩
+  exact ⟨n * m, by positivity, by rwa [pow_mul]⟩
+
+@[to_additive (attr := simp)]
+lemma isOfFinOrder_pow {n : ℕ} : IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0 := by
+  rcases Decidable.eq_or_ne n 0 with rfl | hn
+  · simp
+  · exact ⟨fun h ↦ .inl <| h.of_pow hn, fun h ↦ (h.resolve_right hn).pow⟩
+
 /-- Elements of finite order are of finite order in submonoids. -/
 @[to_additive "Elements of finite order are of finite order in submonoids."]
 theorem Submonoid.isOfFinOrder_coe {H : Submonoid G} {x : H} :
@@ -107,11 +128,6 @@ theorem IsOfFinOrder.apply {η : Type*} {Gs : η → Type*} [∀ i, Monoid (Gs i
   obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one
   exact fun _ => isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩
 
-/-- 1 is of finite order in any monoid. -/
-@[to_additive "0 is of finite order in any additive monoid."]
-theorem isOfFinOrder_one : IsOfFinOrder (1 : G) :=
-  isOfFinOrder_iff_pow_eq_one.mpr ⟨1, Nat.one_pos, one_pow 1⟩
-
 /-- The submonoid generated by an element is a group if that element has finite order. -/
 @[to_additive "The additive submonoid generated by an element is
 an additive group if that element has finite order."]
diff --git a/Mathlib/GroupTheory/Torsion.lean b/Mathlib/GroupTheory/Torsion.lean
index 08d223f5db3ba..2c301f72a0d33 100644
--- a/Mathlib/GroupTheory/Torsion.lean
+++ b/Mathlib/GroupTheory/Torsion.lean
@@ -161,7 +161,7 @@ namespace CommMonoid
 @[to_additive addTorsion "The torsion submonoid of an additive commutative monoid."]
 def torsion : Submonoid G where
   carrier := { x | IsOfFinOrder x }
-  one_mem' := isOfFinOrder_one
+  one_mem' := IsOfFinOrder.one
   mul_mem' hx hy := hx.mul hy
 
 variable {G}