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)
m n : ℤ
⊢ A ^ (m + n) = A ^ m * A ^ n
induction n using Int.induction_on with
| hz => simp
| hp n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
| hn n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
no goals
case hz
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m : ℤ
⊢ A ^ (m + 0) = A ^ m * A ^ 0
simp
no goals
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m : ℤ
n : ℕ
ihn : A ^ (m + ↑n) = A ^ m * A ^ ↑n
⊢ A ^ (m + (↑n + 1)) = A ^ m * A ^ (↑n + 1)
simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
no goals
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m : ℤ
n : ℕ
ihn : A ^ (m + -↑n) = A ^ m * A ^ (-↑n)
⊢ A ^ (m + (-↑n - 1)) = A ^ m * A ^ (-↑n - 1)
rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]