no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ A ^ (↑m * ↑n) = (A ^ ↑m) ^ ↑n
rw [zpow_ofNat, zpow_ofNat, ← pow_mul, ← zpow_ofNat, Int.ofNat_mul]
no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ A ^ (↑m * -[n+1]) = (A ^ ↑m) ^ -[n+1]
rw [zpow_ofNat, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_coe_nat]
no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ A ^ (-[m+1] * ↑n) = (A ^ -[m+1]) ^ ↑n
rw [zpow_ofNat, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_coe_nat,
    inv_pow']
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ IsUnit (det (A ^ ((m + 1) * (n + 1))))
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ A ^ (-[m+1] * -[n+1]) = (A ^ -[m+1]) ^ -[n+1]
rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.ofNat_mul, zpow_ofNat, inv_pow', ←
  pow_mul, nonsing_inv_nonsing_inv]
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ IsUnit (det A ^ ((m + 1) * (n + 1)))
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ IsUnit (det (A ^ ((m + 1) * (n + 1))))
rw [det_pow]
no goals
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ IsUnit (det A ^ ((m + 1) * (n + 1)))
exact h.pow _