Add Commute.orderOf_mul_pow_eq_lcm (#11235)

We add `Commute.orderOf_mul_pow_eq_lcm`: if two commuting elements `x` and `y` of a monoid have order `n` and `m`, there is an element of order `lcm n m`. The result actually gives an explicit (computable) element, written as the product of a power of `x` and a power of `y`.

Co-authored-by: Junyan Xu <[junyanxu.math@gmail.com](mailto:junyanxu.math@gmail.com)>

Mathlib/Data/Nat/Factorization/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.BigOperators.Finsupp
 import Mathlib.Data.Finsupp.Multiset
 import Mathlib.Data.Nat.PrimeFin
 import Mathlib.NumberTheory.Padics.PadicVal
+import Mathlib.Data.Nat.GCD.BigOperators
 import Mathlib.Data.Nat.Interval
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Algebra.GroupPower.Order
@@ -651,6 +652,110 @@ theorem factorization_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
   exact (min_add_max _ _).symm
 #align nat.factorization_lcm Nat.factorization_lcm
 
+/-- If `a = ∏ pᵢ ^ nᵢ` and `b = ∏ pᵢ ^ mᵢ`, then `factorizationLCMLeft = ∏ pᵢ ^ kᵢ`, where
+`kᵢ = nᵢ` if `mᵢ ≤ nᵢ` and `0` otherwise. Note that the product is over the divisors of `lcm a b`,
+so if one of `a` or `b` is `0` then the result is `1`. -/
+def factorizationLCMLeft (a b : ℕ) : ℕ :=
+  (Nat.lcm a b).factorization.prod fun p n ↦
+    if b.factorization p ≤ a.factorization p then p ^ n else 1
+
+/-- If `a = ∏ pᵢ ^ nᵢ` and `b = ∏ pᵢ ^ mᵢ`, then `factorizationLCMRight = ∏ pᵢ ^ kᵢ`, where
+`kᵢ = mᵢ` if `nᵢ < mᵢ` and `0` otherwise. Note that the product is over the divisors of `lcm a b`,
+so if one of `a` or `b` is `0` then the result is `1`.
+
+Note that `factorizationLCMRight a b` is *not* `factorizationLCMLeft b a`: the difference is
+that in `factorizationLCMLeft a b` there are the primes whose exponent in `a` is bigger or equal
+than the exponent in `b`, while in `factorizationLCMRight a b` there are the primes primes whose
+exponent in `b` is strictly bigger than in `a`. For example `factorizationLCMLeft 2 2 = 2`, but
+`factorizationLCMRight 2 2 = 1`. -/
+def factorizationLCMRight (a b : ℕ) :=
+  (Nat.lcm a b).factorization.prod fun p n ↦
+    if b.factorization p ≤ a.factorization p then 1 else p ^ n
+
+variable (a b)
+
+@[simp]
+lemma factorizationLCMLeft_zero_left : factorizationLCMLeft 0 b = 1 := by
+  simp [factorizationLCMLeft]
+
+@[simp]
+lemma factorizationLCMLeft_zero_right : factorizationLCMLeft a 0 = 1 := by
+  simp [factorizationLCMLeft]
+
+@[simp]
+lemma factorizationLCRight_zero_left : factorizationLCMRight 0 b = 1 := by
+  simp [factorizationLCMRight]
+@[simp]
+lemma factorizationLCMRight_zero_right : factorizationLCMRight a 0 = 1 := by
+  simp [factorizationLCMRight]
+
+lemma factorizationLCMLeft_pos :
+    0 < factorizationLCMLeft a b := by
+  apply Nat.pos_of_ne_zero
+  rw [factorizationLCMLeft, Finsupp.prod_ne_zero_iff]
+  intro p _ H
+  by_cases h : b.factorization p ≤ a.factorization p
+  · simp only [h, reduceIte, pow_eq_zero_iff', ne_eq] at H
+    simpa [H.1] using H.2
+  · simp only [h, reduceIte, one_ne_zero] at H
+
+lemma factorizationLCMRight_pos :
+    0 < factorizationLCMRight a b := by
+  apply Nat.pos_of_ne_zero
+  rw [factorizationLCMRight, Finsupp.prod_ne_zero_iff]
+  intro p _ H
+  by_cases h : b.factorization p ≤ a.factorization p
+  · simp only [h, reduceIte, pow_eq_zero_iff', ne_eq] at H
+  · simp only [h, ↓reduceIte, pow_eq_zero_iff', ne_eq] at H
+    simpa [H.1] using H.2
+
+lemma coprime_factorizationLCMLeft_factorizationLCMRight :
+    (factorizationLCMLeft a b).Coprime (factorizationLCMRight a b) := by
+  rw [factorizationLCMLeft, factorizationLCMRight]
+  refine coprime_prod_left_iff.mpr fun p hp ↦ coprime_prod_right_iff.mpr fun q hq ↦ ?_
+  dsimp only; split_ifs with h h'
+  any_goals simp only [coprime_one_right_eq_true, coprime_one_left_eq_true]
+  refine coprime_pow_primes _ _ (prime_of_mem_primeFactors hp) (prime_of_mem_primeFactors hq) ?_
+  contrapose! h'; rwa [← h']
+
+variable {a b}
+
+lemma factorizationLCMLeft_mul_factorizationLCMRight (ha : a ≠ 0) (hb : b ≠ 0) :
+    (factorizationLCMLeft a b) * (factorizationLCMRight a b) = lcm a b := by
+  rw [← factorization_prod_pow_eq_self (lcm_ne_zero ha hb), factorizationLCMLeft,
+    factorizationLCMRight, ← prod_mul]
+  congr; ext p n; split_ifs <;> simp
+
+variable (a b)
+
+lemma factorizationLCMLeft_dvd_left : factorizationLCMLeft a b ∣ a := by
+  rcases eq_or_ne a 0 with rfl | ha
+  · simp only [dvd_zero]
+  rcases eq_or_ne b 0 with rfl | hb
+  · simp [factorizationLCMLeft]
+  nth_rewrite 2 [← factorization_prod_pow_eq_self ha]
+  rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
+  · apply prod_dvd_prod_of_dvd; rintro p -; dsimp only; split_ifs with le
+    · rw [factorization_lcm ha hb]; apply pow_dvd_pow; exact sup_le le_rfl le
+    · apply one_dvd
+  · intro p hp; rw [mem_support_iff] at hp ⊢
+    rw [factorization_lcm ha hb]; exact (lt_sup_iff.mpr <| .inl <| Nat.pos_of_ne_zero hp).ne'
+  · intros; rw [pow_zero]
+
+lemma factorizationLCMRight_dvd_right : factorizationLCMRight a b ∣ b := by
+  rcases eq_or_ne a 0 with rfl | ha
+  · simp [factorizationLCMRight]
+  rcases eq_or_ne b 0 with rfl | hb
+  · simp only [dvd_zero]
+  nth_rewrite 2 [← factorization_prod_pow_eq_self hb]
+  rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
+  · apply Finset.prod_dvd_prod_of_dvd; rintro p -; dsimp only; split_ifs with le
+    · apply one_dvd
+    · rw [factorization_lcm ha hb]; apply pow_dvd_pow; exact sup_le (not_le.1 le).le le_rfl
+  · intro p hp; rw [mem_support_iff] at hp ⊢
+    rw [factorization_lcm ha hb]; exact (lt_sup_iff.mpr <| .inr <| Nat.pos_of_ne_zero hp).ne'
+  · intros; rw [pow_zero]
+
 @[to_additive sum_primeFactors_gcd_add_sum_primeFactors_mul]
 theorem prod_primeFactors_gcd_mul_prod_primeFactors_mul {β : Type*} [CommMonoid β] (m n : ℕ)
     (f : ℕ → β) :

Mathlib/GroupTheory/Exponent.lean

@@ -286,6 +286,41 @@ theorem _root_.Nat.Prime.exists_orderOf_eq_pow_factorization_exponent {p : ℕ}
 #align nat.prime.exists_order_of_eq_pow_factorization_exponent Nat.Prime.exists_orderOf_eq_pow_factorization_exponent
 #align nat.prime.exists_order_of_eq_pow_padic_val_nat_add_exponent Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent
 
+variable {G} in
+open Nat in
+/-- If two commuting elements `x` and `y` of a monoid have order `n` and `m`, there is an element
+of order `lcm n m`. The result actually gives an explicit (computable) element, written as the
+product of a power of `x` and a power of `y`. See also the result below if you don't need the
+explicit formula. -/
+@[to_additive "If two commuting elements `x` and `y` of an additive monoid have order `n` and `m`,
+there is an element of order `lcm n m`. The result actually gives an explicit (computable) element,
+written as the sum of a multiple of `x` and a multiple of `y`. See also the result below if you
+don't need the explicit formula."]
+lemma _root_.Commute.orderOf_mul_pow_eq_lcm {x y : G} (h : Commute x y) (hx : orderOf x ≠ 0)
+    (hy : orderOf y ≠ 0) :
+    orderOf (x ^ (orderOf x / (factorizationLCMLeft (orderOf x) (orderOf y))) *
+      y ^ (orderOf y / factorizationLCMRight (orderOf x) (orderOf y))) =
+      Nat.lcm (orderOf x) (orderOf y) := by
+  rw [(h.pow_pow _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
+  all_goals iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
+  all_goals simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
+    factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]
+
+open Submonoid in
+/-- If two commuting elements `x` and `y` of a monoid have order `n` and `m`, then there is an
+element of order `lcm n m` that lies in the subgroup generated by `x` and `y`. -/
+@[to_additive "If two commuting elements `x` and `y` of an additive monoid have order `n` and `m`,
+then there is an element of order `lcm n m` that lies in the additive subgroup generated by `x`
+and `y`."]
+theorem _root_.Commute.exists_orderOf_eq_lcm {x y : G} (h : Commute x y) :
+    ∃ z ∈ closure {x, y}, orderOf z = Nat.lcm (orderOf x) (orderOf y) := by
+  by_cases hx : orderOf x = 0 <;> by_cases hy : orderOf y = 0
+  · exact ⟨x, subset_closure (by simp), by simp [hx]⟩
+  · exact ⟨x, subset_closure (by simp), by simp [hx]⟩
+  · exact ⟨y, subset_closure (by simp), by simp [hy]⟩
+  · exact ⟨_, mul_mem (pow_mem (subset_closure (by simp)) _) (pow_mem (subset_closure (by simp)) _),
+      h.orderOf_mul_pow_eq_lcm hx hy⟩
+
 /-- A nontrivial monoid has prime exponent `p` if and only if every non-identity element has
 order `p`. -/
 @[to_additive]

Mathlib/GroupTheory/OrderOfElement.lean

@@ -405,6 +405,16 @@ theorem orderOf_pow' (h : n ≠ 0) : orderOf (x ^ n) = orderOf x / gcd (orderOf
 #align order_of_pow' orderOf_pow'
 #align add_order_of_nsmul' addOrderOf_nsmul'
 
+@[to_additive]
+lemma orderOf_pow_of_dvd {x : G} {n : ℕ} (hn : n ≠ 0) (dvd : n ∣ orderOf x) :
+    orderOf (x ^ n) = orderOf x / n := by rw [orderOf_pow' _ hn, Nat.gcd_eq_right dvd]
+
+@[to_additive]
+lemma orderOf_pow_orderOf_div {x : G} {n : ℕ} (hx : orderOf x ≠ 0) (hn : n ∣ orderOf x) :
+    orderOf (x ^ (orderOf x / n)) = n := by
+  rw [orderOf_pow_of_dvd _ (Nat.div_dvd_of_dvd hn), Nat.div_div_self hn hx]
+  rw [← Nat.div_mul_cancel hn] at hx; exact left_ne_zero_of_mul hx
+
 variable (n)
 
 @[to_additive]