case zero
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ adjugate (A ^ Nat.zero) = adjugate A ^ Nat.zero

case succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
IH : adjugate (A ^ k) = adjugate A ^ k
⊢ adjugate (A ^ Nat.succ k) = adjugate A ^ Nat.succ k
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
⊢ adjugate (A ^ k) = adjugate A ^ k
induction' k with k IH
no goals
case zero
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ adjugate (A ^ Nat.zero) = adjugate A ^ Nat.zero
simp
no goals
case succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
IH : adjugate (A ^ k) = adjugate A ^ k
⊢ adjugate (A ^ Nat.succ k) = adjugate A ^ Nat.succ k
rw [pow_succ', mul_eq_mul, adjugate_mul_distrib, IH, ← mul_eq_mul, pow_succ]