G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
⊢ (fun x_1 => x ^ n * x_1) 1 = 1 ↔ x ^ n = 1
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
⊢ IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1 ↔ x ^ n = 1
rw [IsPeriodicPt, IsFixedPt, mul_left_iterate]
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x : G
⊢ (fun x_1 => x ^ n * x_1) 1 = 1 ↔ x ^ n = 1
simp only [mul_one]