no goals
α : Type ?u.106815
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a
simp only [← Int.ofNat_succ, zpow_ofNat, pow_succ']
no goals
α : Type ?u.106815
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
⊢ a ^ (-[0+1] + 1) = a ^ -[0+1] * a
erw [zpow_zero, zpow_negSucc, pow_one, mul_left_inv]
α : Type ?u.106815
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-[n + 1+1] + 1) = (a ^ (n + 1))⁻¹
α : Type ?u.106815
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-[n + 1+1] + 1) = a ^ -[n + 1+1] * a
rw [zpow_negSucc, pow_succ, mul_inv_rev, inv_mul_cancel_right]
α : Type ?u.106815
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-↑(n + 1)) = (a ^ (n + 1))⁻¹
α : Type ?u.106815
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-[n + 1+1] + 1) = (a ^ (n + 1))⁻¹
rw [Int.negSucc_eq, neg_add, add_assoc, neg_add_self, add_zero]
no goals
α : Type ?u.106815
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-↑(n + 1)) = (a ^ (n + 1))⁻¹
exact zpow_negSucc _ _