[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
⊢ Monoid M
[PROOFSTEP]
infer_instance
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
src✝ : Monoid M :=
  let_fun this := inferInstance;
  this
⊢ Inv M
[PROOFSTEP]
infer_instance
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ n = (A ^ n)⁻¹
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A⁻¹ ^ Nat.zero = (A ^ Nat.zero)⁻¹
[PROOFSTEP]
simp
[GOAL]
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
⊢ A⁻¹ ^ Nat.succ n = (A ^ Nat.succ n)⁻¹
[PROOFSTEP]
rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit (det A)
h : n ≤ m
⊢ A ^ (m - n) = A ^ m * (A ^ n)⁻¹
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, pow_add, Matrix.mul_assoc, mul_nonsing_inv, tsub_add_cancel_of_le h, Matrix.mul_one]
[GOAL]
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit (det A)
h : n ≤ m
⊢ IsUnit (det (A ^ n))
[PROOFSTEP]
simpa using ha.pow n
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
⊢ A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
[PROOFSTEP]
induction' n with n IH generalizing m
[GOAL]
case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ m : ℕ
⊢ A⁻¹ ^ m * A ^ Nat.zero = A ^ Nat.zero * A⁻¹ ^ m
[PROOFSTEP]
simp
[GOAL]
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
⊢ A⁻¹ ^ m * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ m
[PROOFSTEP]
cases' m with m m
[GOAL]
case succ.zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
⊢ A⁻¹ ^ Nat.zero * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ.succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
⊢ A⁻¹ ^ Nat.succ m * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ Nat.succ m
[PROOFSTEP]
rcases nonsing_inv_cancel_or_zero A with (⟨h, h'⟩ | h)
[GOAL]
case succ.succ.inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ Nat.succ m * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ Nat.succ m
[PROOFSTEP]
simp only [Nat.succ_eq_add_one]
[GOAL]
case succ.succ.inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
[PROOFSTEP]
calc
  A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
    simp only [pow_succ' A⁻¹, pow_succ A, Matrix.mul_assoc]
  _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, Matrix.one_mul, IH m]
  _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one, Matrix.one_mul]
  _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by simp only [pow_succ' A, pow_succ A⁻¹, Matrix.mul_assoc]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n
[PROOFSTEP]
simp only [pow_succ' A⁻¹, pow_succ A, Matrix.mul_assoc]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ m * (A⁻¹ * A) * A ^ n = A ^ n * A⁻¹ ^ m
[PROOFSTEP]
simp only [h, Matrix.mul_one, Matrix.one_mul, IH m]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A ^ n * A⁻¹ ^ m = A ^ n * (A * A⁻¹) * A⁻¹ ^ m
[PROOFSTEP]
simp only [h', Matrix.mul_one, Matrix.one_mul]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A ^ n * (A * A⁻¹) * A⁻¹ ^ m = A ^ (n + 1) * A⁻¹ ^ (m + 1)
[PROOFSTEP]
simp only [pow_succ' A, pow_succ A⁻¹, Matrix.mul_assoc]
[GOAL]
case succ.succ.inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ = 0
⊢ A⁻¹ ^ Nat.succ m * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ Nat.succ m
[PROOFSTEP]
simp [h]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ 1 ^ ↑n = 1
[PROOFSTEP]
rw [zpow_ofNat, one_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ 1 ^ -[n+1] = 1
[PROOFSTEP]
rw [zpow_negSucc, one_pow, inv_one]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0
[PROOFSTEP]
rw [zpow_ofNat, zero_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : ↑n ≠ 0
⊢ 0 < n
[PROOFSTEP]
refine' lt_of_le_of_ne n.zero_le (Ne.symm _)
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
simpa using h
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
x✝ : -[n+1] ≠ 0
⊢ 0 ^ -[n+1] = 0
[PROOFSTEP]
simp [zero_pow n.zero_lt_succ]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : n = 0
⊢ 0 ^ n = 1
[PROOFSTEP]
rw [h, zpow_zero]
[GOAL]
case neg
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0
[PROOFSTEP]
rw [zero_zpow _ h]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ ↑n = (A ^ ↑n)⁻¹
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, inv_pow']
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ -[n+1] = (A ^ -[n+1])⁻¹
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, inv_pow']
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A ^ (-1) = A⁻¹
[PROOFSTEP]
convert DivInvMonoid.zpow_neg' 0 A
[GOAL]
case h.e'_3.h.e'_3
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A = DivInvMonoid.zpow (↑(Nat.succ 0)) A
[PROOFSTEP]
simp only [zpow_one, Int.ofNat_zero, Int.ofNat_succ, zpow_eq_pow, zero_add]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A ^ (-↑n) = (A ^ n)⁻¹
[PROOFSTEP]
cases n
[GOAL]
case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A ^ (-↑Nat.zero) = (A ^ Nat.zero)⁻¹
[PROOFSTEP]
simp
[GOAL]
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n✝ : ℕ
⊢ A ^ (-↑(Nat.succ n✝)) = (A ^ Nat.succ n✝)⁻¹
[PROOFSTEP]
exact DivInvMonoid.zpow_neg' _ _
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ IsUnit (det (A ^ n))
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ IsUnit (det (A ^ ofNat n))
[PROOFSTEP]
simpa using h.pow n
[GOAL]
case negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ IsUnit (det (A ^ -[n+1]))
[PROOFSTEP]
simpa using h.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℤ
⊢ IsUnit (det (A ^ z)) ↔ IsUnit (det A) ∨ z = 0
[PROOFSTEP]
induction' z using Int.induction_on with z _ z _
[GOAL]
case hz
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ IsUnit (det (A ^ 0)) ↔ IsUnit (det A) ∨ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ ↑z)) ↔ IsUnit (det A) ∨ ↑z = 0
⊢ IsUnit (det (A ^ (↑z + 1))) ↔ IsUnit (det A) ∨ ↑z + 1 = 0
[PROOFSTEP]
rw [← Int.ofNat_succ, zpow_ofNat, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero, Int.ofNat_inj]
[GOAL]
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ ↑z)) ↔ IsUnit (det A) ∨ ↑z = 0
⊢ IsUnit (det A) ↔ IsUnit (det A) ∨ Nat.succ z = 0
[PROOFSTEP]
simp
[GOAL]
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ (-↑z))) ↔ IsUnit (det A) ∨ -↑z = 0
⊢ IsUnit (det (A ^ (-↑z - 1))) ↔ IsUnit (det A) ∨ -↑z - 1 = 0
[PROOFSTEP]
rw [← neg_add', ← Int.ofNat_succ, zpow_neg_coe_nat, isUnit_nonsing_inv_det_iff, det_pow, isUnit_pow_succ_iff,
  neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]
[GOAL]
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ (-↑z))) ↔ IsUnit (det A) ∨ -↑z = 0
⊢ IsUnit (det A) ↔ IsUnit (det A) ∨ Nat.succ z = 0
[PROOFSTEP]
simp
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ A ^ (- -[n+1]) = (A ^ -[n+1])⁻¹
[PROOFSTEP]
rw [zpow_negSucc, neg_negSucc, zpow_ofNat, nonsing_inv_nonsing_inv]
[GOAL]
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)
n : ℕ
⊢ IsUnit (det (A ^ (n + 1)))
[PROOFSTEP]
rw [det_pow]
[GOAL]
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)
n : ℕ
⊢ IsUnit (det A ^ (n + 1))
[PROOFSTEP]
exact h.pow _
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ A⁻¹ ^ n = A ^ (-n)
[PROOFSTEP]
rw [zpow_neg h, inv_zpow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ A ^ (↑n + 1) = A ^ ↑n * A
[PROOFSTEP]
simp only [← Nat.cast_succ, pow_succ', zpow_ofNat]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ A ^ (-(↑n + 1) + 1) = (A ^ n)⁻¹
[PROOFSTEP]
rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_ofNat]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ (A ^ n)⁻¹ = (A * A ^ n)⁻¹ * A
[PROOFSTEP]
rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ (A * A ^ n)⁻¹ * A = A ^ (-(↑n + 1)) * A
[PROOFSTEP]
rw [zpow_neg h, ← Int.ofNat_succ, zpow_ofNat, pow_succ]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹
[PROOFSTEP]
rw [mul_assoc, mul_nonsing_inv _ h, mul_one]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ A ^ (n - 1) * A * A⁻¹ = A ^ n * A⁻¹
[PROOFSTEP]
rw [← zpow_add_one h, sub_add_cancel]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]

| hz => simp
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]

| hp n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
[GOAL]
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)
[PROOFSTEP]
simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
[GOAL]
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)
[PROOFSTEP]

| hn n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
[GOAL]
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)
[PROOFSTEP]
rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)
[GOAL]
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ * A = 1
right✝ : A * A⁻¹ = 1
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
exact zpow_add (isUnit_det_of_left_inverse h) m n
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ = 0
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := exists_eq_neg_ofNat hm
[GOAL]
case inr.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : n ≤ 0
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
⊢ A ^ (-↑k + n) = A ^ (-↑k) * A ^ n
[PROOFSTEP]
obtain ⟨l, rfl⟩ := exists_eq_neg_ofNat hn
[GOAL]
case inr.intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A ^ (-↑k + -↑l) = A ^ (-↑k) * A ^ (-↑l)
[PROOFSTEP]
simp_rw [← neg_add, ← Int.ofNat_add, zpow_neg_coe_nat, ← inv_pow', h, pow_add]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : 0 ≤ m
hn : 0 ≤ n
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm
[GOAL]
case intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : 0 ≤ n
k : ℕ
hm : 0 ≤ ↑k
⊢ A ^ (↑k + n) = A ^ ↑k * A ^ n
[PROOFSTEP]
obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn
[GOAL]
case intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
k : ℕ
hm : 0 ≤ ↑k
l : ℕ
hn : 0 ≤ ↑l
⊢ A ^ (↑k + ↑l) = A ^ ↑k * A ^ ↑l
[PROOFSTEP]
rw [← Int.ofNat_add, zpow_ofNat, zpow_ofNat, zpow_ofNat, pow_add]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
i : ℤ
⊢ A ^ (1 + i) = A * A ^ i
[PROOFSTEP]
rw [zpow_add h, zpow_one]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ SemiconjBy A (X ^ ↑n) (Y ^ ↑n)
[PROOFSTEP]
simp [h.pow_right n]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
[PROOFSTEP]
have hx' : IsUnit (X ^ n.succ).det := by
  rw [det_pow]
  exact hx.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (det (X ^ Nat.succ n))
[PROOFSTEP]
rw [det_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (det X ^ Nat.succ n)
[PROOFSTEP]
exact hx.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
[PROOFSTEP]
have hy' : IsUnit (Y ^ n.succ).det := by
  rw [det_pow]
  exact hy.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ IsUnit (det (Y ^ Nat.succ n))
[PROOFSTEP]
rw [det_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ IsUnit (det Y ^ Nat.succ n)
[PROOFSTEP]
exact hy.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, nonsing_inv_apply _ hx', nonsing_inv_apply _ hy', SemiconjBy]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n) = ↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A
[PROOFSTEP]
refine' (isRegular_of_isLeftRegular_det hy'.isRegular.left).left _
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ (fun x => Y ^ Nat.succ n * x) (A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n)) =
    (fun x => Y ^ Nat.succ n * x) (↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A)
[PROOFSTEP]
dsimp only
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ Y ^ Nat.succ n * (A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n)) =
    Y ^ Nat.succ n * (↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A)
[PROOFSTEP]
rw [← mul_assoc, ← (h.pow_right n.succ).eq, mul_assoc, mul_smul, mul_adjugate, ← Matrix.mul_assoc,
  mul_smul (Y ^ _) (↑hy'.unit⁻¹ : R), mul_adjugate, smul_smul, smul_smul, hx'.val_inv_mul, hy'.val_inv_mul, one_smul,
  Matrix.mul_one, Matrix.one_mul]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
⊢ Commute A (B ^ m)
[PROOFSTEP]
rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)
[GOAL]
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ Commute A (B ^ m)
[PROOFSTEP]
refine' SemiconjBy.zpow_right _ _ h _
[GOAL]
case inl.intro.refine'_1
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ IsUnit (det B)
[PROOFSTEP]
exact isUnit_det_of_left_inverse hB
[GOAL]
case inl.intro.refine'_2
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ IsUnit (det B)
[PROOFSTEP]
exact isUnit_det_of_left_inverse hB
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
⊢ Commute A (B ^ m)
[PROOFSTEP]
cases m
[GOAL]
case inr.ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ ofNat a✝)
[PROOFSTEP]
simpa using h.pow_right _
[GOAL]
case inr.negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ -[a✝+1])
[PROOFSTEP]
simp [← inv_pow', hB]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ A ^ bit0 n = A ^ n * A ^ n
[PROOFSTEP]
cases' le_total 0 n with nonneg nonpos
[GOAL]
case inl
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
nonneg : 0 ≤ n
⊢ A ^ bit0 n = A ^ n * A ^ n
[PROOFSTEP]
exact zpow_add_of_nonneg nonneg nonneg
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
nonpos : n ≤ 0
⊢ A ^ bit0 n = A ^ n * A ^ n
[PROOFSTEP]
exact zpow_add_of_nonpos nonpos nonpos
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : ↑n ≠ -1
⊢ A ^ (↑n + 1) = A ^ ↑n * A
[PROOFSTEP]
simp only [pow_succ', ← Nat.cast_succ, zpow_ofNat]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A
[PROOFSTEP]
rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)
[GOAL]
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ * A = 1
right✝ : A * A⁻¹ = 1
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A
[PROOFSTEP]
apply zpow_add_one (isUnit_det_of_left_inverse h)
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A
[PROOFSTEP]
show A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * A
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-↑(n + 1)) = A ^ (-↑(n + 2)) * A
[PROOFSTEP]
simp_rw [zpow_neg_coe_nat, ← inv_pow', h, zero_pow Nat.succ_pos', zero_mul]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ A ^ bit1 n = A ^ n * A ^ n * A
[PROOFSTEP]
rw [bit1, zpow_add_one_of_ne_neg_one, zpow_bit0]
[GOAL]
case a
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ bit0 n ≠ -1
[PROOFSTEP]
intro h
[GOAL]
case a
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
h : bit0 n = -1
⊢ False
[PROOFSTEP]
simpa using congr_arg bodd h
[GOAL]
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
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, ← pow_mul, ← zpow_ofNat, Int.ofNat_mul]
[GOAL]
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]
[PROOFSTEP]
rw [zpow_ofNat, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_coe_nat]
[GOAL]
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
[PROOFSTEP]
rw [zpow_ofNat, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_coe_nat, inv_pow']
[GOAL]
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]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.ofNat_mul, zpow_ofNat, inv_pow', ← pow_mul,
  nonsing_inv_nonsing_inv]
[GOAL]
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))))
[PROOFSTEP]
rw [det_pow]
[GOAL]
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)))
[PROOFSTEP]
exact h.pow _
[GOAL]
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 ^ n) ^ m
[PROOFSTEP]
rw [mul_comm, zpow_mul _ h]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
n : ℕ
⊢ ↑(u ^ ↑n) = ↑u ^ ↑n
[PROOFSTEP]
rw [_root_.zpow_coe_nat, zpow_ofNat, Units.val_pow_eq_pow_val]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
k : ℕ
⊢ ↑(u ^ -[k+1]) = ↑u ^ -[k+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]
[GOAL]
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
⊢ A ^ z ≠ 0
[PROOFSTEP]
have := ha.det_zpow z
[GOAL]
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : IsUnit (det (A ^ z))
⊢ A ^ z ≠ 0
[PROOFSTEP]
contrapose! this
[GOAL]
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit (det (A ^ z))
[PROOFSTEP]
rw [this, det_zero ‹_›]
[GOAL]
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit 0
[PROOFSTEP]
exact not_isUnit_zero
[GOAL]
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
[PROOFSTEP]
rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
n : ℕ
⊢ (A * B) ^ ↑n = A ^ ↑n * B ^ ↑n
[PROOFSTEP]
simp [h.mul_pow n]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
n : ℕ
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, ← mul_inv_rev, h.mul_pow n.succ, (h.pow_pow _ _).eq]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ A ^ bit1 n = (A * A) ^ n * A
[PROOFSTEP]
rw [zpow_bit1, Commute.mul_zpow (Commute.refl A)]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
A : M
h : IsUnit (det A)
⊢ A ^ (-n) * A ^ n = 1
[PROOFSTEP]
rw [zpow_neg h, nonsing_inv_mul _ (h.det_zpow _)]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (1 / A) ^ n = 1 / A ^ n
[PROOFSTEP]
simp only [one_div, inv_pow']
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ (1 / A) ^ n = 1 / A ^ n
[PROOFSTEP]
simp only [one_div, inv_zpow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ ↑n)ᵀ = Aᵀ ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, transpose_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᵀ = Aᵀ ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]
[GOAL]
n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ ↑n)ᴴ = Aᴴ ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, conjTranspose_pow]
[GOAL]
n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᴴ = Aᴴ ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]
