G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 => x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 => x * x_1) 1 / gcd (minimalPeriod (fun x_1 => x * x_1) 1) n
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : IsOfFinOrder x
⊢ orderOf (x ^ n) = orderOf x / gcd (orderOf x) n
unfold orderOf
no goals
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 => x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 => x * x_1) 1 / gcd (minimalPeriod (fun x_1 => x * x_1) 1) n
rw [← minimalPeriod_iterate_eq_div_gcd' h, mul_left_iterate]