case a.h
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
i j : n
⊢ adjugate A i j = OfNat.ofNat 1 i j
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
⊢ adjugate A = 1
ext (i j)
no goals
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
i j : n
⊢ adjugate A i j = OfNat.ofNat 1 i j
simp [Subsingleton.elim i j, adjugate_apply, det_eq_elem_of_subsingleton _ i]