no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
z1 z2 : ℤ
⊢ A ^ (z1 - z2) = A ^ z1 / A ^ z2
rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]