English
If x and y commute, y has finite order, and every prime p dividing orderOf x also divides orderOf y in a strong sense, then orderOf(x y) = orderOf(y).
Русский
Если x и y commute, у y конечный порядок, и для каждого простого p, делящего orderOf(x), выполняется соответствующее условие делимости, то orderOf(x y) = orderOf(y).
LaTeX
$$Forall p (Prime(p) → p ∣ orderOf(x) → p * orderOf(x) ∣ orderOf(y)) → orderOf(x y) = orderOf(y)$$
Lean4
/-- If each prime factor of `orderOf x` has higher multiplicity in `orderOf y`, and `x` commutes
with `y`, then `x * y` has the same order as `y`. -/
@[to_additive addOrderOf_add_eq_right_of_forall_prime_mul_dvd /-- If each prime factor of
`addOrderOf x` has higher multiplicity in `addOrderOf y`, and `x` commutes with `y`,
then `x + y` has the same order as `y`. -/
]
theorem orderOf_mul_eq_right_of_forall_prime_mul_dvd (h : Commute x y) (hy : IsOfFinOrder y)
(hdvd : ∀ p : ℕ, p.Prime → p ∣ orderOf x → p * orderOf x ∣ orderOf y) : orderOf (x * y) = orderOf y :=
by
have hoy := hy.orderOf_pos
have hxy := dvd_of_forall_prime_mul_dvd hdvd
apply orderOf_eq_of_pow_and_pow_div_prime hoy <;> simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]
· exact h.orderOf_mul_dvd_lcm.trans (lcm_dvd hxy dvd_rfl)
refine fun p hp hpy hd => hp.ne_one ?_
rw [← Nat.dvd_one, ← mul_dvd_mul_iff_right hoy.ne', one_mul, ← dvd_div_iff_mul_dvd hpy]
refine (orderOf_dvd_lcm_mul h).trans (lcm_dvd ((dvd_div_iff_mul_dvd hpy).2 ?_) hd)
by_cases h : p ∣ orderOf x
exacts [hdvd p hp h, (hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy]
