case h
m : Type ?u.177310
n : Type u_1
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
R : Type v
inst✝¹ : CommRing R
inst✝ : IsEmpty n
x✝ : Matrix n n R
⊢ det x✝ = const (Matrix n n R) 1 x✝
m : Type ?u.177310
n : Type u_1
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
R : Type v
inst✝¹ : CommRing R
inst✝ : IsEmpty n
⊢ det = const (Matrix n n R) 1
ext
no goals
case h
m : Type ?u.177310
n : Type u_1
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
R : Type v
inst✝¹ : CommRing R
inst✝ : IsEmpty n
x✝ : Matrix n n R
⊢ det x✝ = const (Matrix n n R) 1 x✝
exact det_isEmpty