no goals
α : Type u_1
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✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ bit0 ↑n = a ^ ↑n * a ^ ↑n
simp only [zpow_ofNat, ← Int.ofNat_bit0, pow_bit0]
α : Type u_1
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✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ bit0 -[n+1] = (a ^ bit0 (n + 1))⁻¹
α : Type u_1
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✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ bit0 -[n+1] = a ^ -[n+1] * a ^ -[n+1]
simp [← mul_inv_rev, ← pow_bit0]
α : Type u_1
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✝ : DivisionMonoid α
a : α
n : ℕ
⊢ (a ^ bit0 (↑n + 1))⁻¹ = (a ^ bit0 (n + 1))⁻¹
α : Type u_1
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✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ bit0 -[n+1] = (a ^ bit0 (n + 1))⁻¹
rw [negSucc_eq, bit0_neg, zpow_neg]
no goals
α : Type u_1
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✝ : DivisionMonoid α
a : α
n : ℕ
⊢ (a ^ bit0 (↑n + 1))⁻¹ = (a ^ bit0 (n + 1))⁻¹
norm_cast