α : Type ?u.121034
β : Type ?u.121037
m : Type u_1
n : Type ?u.121043
o : Type ?u.121046
m' : α → Type ?u.121051
n' : α → Type ?u.121056
R : Type v
inst✝⁵ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : LinearOrder m
h : BlockTriangular M id
this : DecidableEq R
⊢ det M = ∏ i : m, M i i
α : Type ?u.121034
β : Type ?u.121037
m : Type u_1
n : Type ?u.121043
o : Type ?u.121046
m' : α → Type ?u.121051
n' : α → Type ?u.121056
R : Type v
inst✝⁵ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : LinearOrder m
h : BlockTriangular M id
⊢ det M = ∏ i : m, M i i
haveI : DecidableEq R := Classical.decEq _
no goals
α : Type ?u.121034
β : Type ?u.121037
m : Type u_1
n : Type ?u.121043
o : Type ?u.121046
m' : α → Type ?u.121051
n' : α → Type ?u.121056
R : Type v
inst✝⁵ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : LinearOrder m
h : BlockTriangular M id
this : DecidableEq R
⊢ det M = ∏ i : m, M i i
simp_rw [h.det, image_id, det_toSquareBlock_id]