no goals
n' : Type u_2
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ ↑n)ᴴ = Aᴴ ^ ↑n
rw [zpow_ofNat, zpow_ofNat, conjTranspose_pow]
no goals
n' : Type u_2
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᴴ = Aᴴ ^ -[n+1]
rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]