case ofNat
α : Type u_2
β : Type u_1
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ Int.ofNat a✝

case negSucc
α : Type u_2
β : Type u_1
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ Int.negSucc a✝
α : Type u_2
β : Type u_1
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℤ
⊢ a ^ n • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ n
cases n
no goals
case ofNat
α : Type u_2
β : Type u_1
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ Int.ofNat a✝
rw [Int.ofNat_eq_coe, zpow_ofNat, Int.coe_nat_dvd, pow_smul_eq_iff_minimalPeriod_dvd]
no goals
case negSucc
α : Type u_2
β : Type u_1
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ • b = b ↔ ↑(minimalPeriod ((fun x x_1 => x • x_1) a) b) ∣ Int.negSucc a✝
rw [Int.negSucc_coe, zpow_neg, zpow_ofNat, inv_smul_eq_iff, eq_comm, dvd_neg, Int.coe_nat_dvd,
  pow_smul_eq_iff_minimalPeriod_dvd]