α : Type ?u.59918
β : Type ?u.59921
m : Type u_1
n : Type ?u.59927
o : Type ?u.59930
m' : α → Type ?u.59935
n' : α → Type ?u.59940
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ det
      (fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
        (toBlock M (fun j => ¬p j) fun j => ¬p j)) =
    det (toSquareBlockProp M p) * det (toSquareBlockProp M fun i => ¬p i)
α : Type ?u.59918
β : Type ?u.59921
m : Type u_1
n : Type ?u.59927
o : Type ?u.59930
m' : α → Type ?u.59935
n' : α → Type ?u.59940
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ det M = det (toSquareBlockProp M p) * det (toSquareBlockProp M fun i => ¬p i)
rw [det_toBlock M p]
case h.e'_2.h.e'_6.h.e'_8
α : Type ?u.59918
β : Type ?u.59921
m : Type u_1
n : Type ?u.59927
o : Type ?u.59930
m' : α → Type ?u.59935
n' : α → Type ?u.59940
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ toBlock M (fun j => ¬p j) p = 0
α : Type ?u.59918
β : Type ?u.59921
m : Type u_1
n : Type ?u.59927
o : Type ?u.59930
m' : α → Type ?u.59935
n' : α → Type ?u.59940
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ det
      (fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
        (toBlock M (fun j => ¬p j) fun j => ¬p j)) =
    det (toSquareBlockProp M p) * det (toSquareBlockProp M fun i => ¬p i)
convert det_fromBlocks_zero₂₁ (toBlock M p p) (toBlock M p fun j => ¬p j)
    (toBlock M (fun j => ¬p j) fun j => ¬p j)
case h.e'_2.h.e'_6.h.e'_8.a.h
α : Type ?u.59918
β : Type ?u.59921
m : Type u_1
n : Type ?u.59927
o : Type ?u.59930
m' : α → Type ?u.59935
n' : α → Type ?u.59940
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
i : { a // ¬p a }
j : { a // p a }
⊢ toBlock M (fun j => ¬p j) p i j = OfNat.ofNat 0 i j
case h.e'_2.h.e'_6.h.e'_8
α : Type ?u.59918
β : Type ?u.59921
m : Type u_1
n : Type ?u.59927
o : Type ?u.59930
m' : α → Type ?u.59935
n' : α → Type ?u.59940
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ toBlock M (fun j => ¬p j) p = 0
ext i j
no goals
case h.e'_2.h.e'_6.h.e'_8.a.h
α : Type ?u.59918
β : Type ?u.59921
m : Type u_1
n : Type ?u.59927
o : Type ?u.59930
m' : α → Type ?u.59935
n' : α → Type ?u.59940
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
i : { a // ¬p a }
j : { a // p a }
⊢ toBlock M (fun j => ¬p j) p i j = OfNat.ofNat 0 i j
exact h (↑i) i.2 (↑j) j.2