case intro.inl
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1

case intro.inr
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
⊢ ↑(orderOf x) ∣ i ↔ x ^ i = 1
rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩
no goals
case intro.inl
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1
rw [Int.coe_nat_dvd, orderOf_dvd_iff_pow_eq_one, zpow_ofNat]
no goals
case intro.inr
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1
rw [dvd_neg, Int.coe_nat_dvd, zpow_neg, inv_eq_one, zpow_ofNat, orderOf_dvd_iff_pow_eq_one]