G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
⊢ minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 ∣ lcm (orderOf x) (orderOf y)
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
⊢ orderOf (x * y) ∣ lcm (orderOf x) (orderOf y)
rw [orderOf, ← comp_mul_left]
no goals
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
⊢ minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 ∣ lcm (orderOf x) (orderOf y)
exact Function.Commute.minimalPeriod_of_comp_dvd_lcm h.function_commute_mul_left