α : Type u_1
β : Type ?u.117449
m : Type u_2
n : Type ?u.117455
o : Type ?u.117458
m' : α → Type ?u.117463
n' : α → Type ?u.117468
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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : BlockTriangular M b
a : α
x✝ : a ∈ univ
ha : ¬a ∈ image b univ
⊢ det (toSquareBlock M b a) = 1
α : Type u_1
β : Type ?u.117449
m : Type u_2
n : Type ?u.117455
o : Type ?u.117458
m' : α → Type ?u.117463
n' : α → Type ?u.117468
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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : BlockTriangular M b
⊢ det M = ∏ k : α, det (toSquareBlock M b k)
refine' h.det.trans (prod_subset (subset_univ _) fun a _ ha => _)
α : Type u_1
β : Type ?u.117449
m : Type u_2
n : Type ?u.117455
o : Type ?u.117458
m' : α → Type ?u.117463
n' : α → Type ?u.117468
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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : BlockTriangular M b
a : α
x✝ : a ∈ univ
ha : ¬a ∈ image b univ
this : IsEmpty { i // b i = a }
⊢ det (toSquareBlock M b a) = 1
α : Type u_1
β : Type ?u.117449
m : Type u_2
n : Type ?u.117455
o : Type ?u.117458
m' : α → Type ?u.117463
n' : α → Type ?u.117468
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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : BlockTriangular M b
a : α
x✝ : a ∈ univ
ha : ¬a ∈ image b univ
⊢ det (toSquareBlock M b a) = 1
have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩
no goals
α : Type u_1
β : Type ?u.117449
m : Type u_2
n : Type ?u.117455
o : Type ?u.117458
m' : α → Type ?u.117463
n' : α → Type ?u.117468
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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : BlockTriangular M b
a : α
x✝ : a ∈ univ
ha : ¬a ∈ image b univ
this : IsEmpty { i // b i = a }
⊢ det (toSquareBlock M b a) = 1
exact det_isEmpty