α : Type ?u.123418
β : Type ?u.123421
m : Type u_1
n : Type ?u.123427
o : Type ?u.123430
m' : α → Type ?u.123435
n' : α → Type ?u.123440
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
M : Matrix m m R
h : BlockTriangular M ↑toDual
⊢ det Mᵀ = ∏ i : m, M i i
α : Type ?u.123418
β : Type ?u.123421
m : Type u_1
n : Type ?u.123427
o : Type ?u.123430
m' : α → Type ?u.123435
n' : α → Type ?u.123440
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
M : Matrix m m R
h : BlockTriangular M ↑toDual
⊢ det M = ∏ i : m, M i i
rw [← det_transpose]
no goals
α : Type ?u.123418
β : Type ?u.123421
m : Type u_1
n : Type ?u.123427
o : Type ?u.123430
m' : α → Type ?u.123435
n' : α → Type ?u.123440
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
M : Matrix m m R
h : BlockTriangular M ↑toDual
⊢ det Mᵀ = ∏ i : m, M i i
exact det_of_upperTriangular h.transpose