case a.h
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j : n
⊢ adjugate 0 i j = OfNat.ofNat 0 i j
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Nontrivial n
⊢ adjugate 0 = 0
ext (i j)
case a.h.intro
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ adjugate 0 i j = OfNat.ofNat 0 i j
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j : n
⊢ adjugate 0 i j = OfNat.ofNat 0 i j
obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j
case a.h.intro
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), updateColumn 0ᵀ j (Pi.single i 1) i_1 j' = 0
case a.h.intro
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ adjugate 0 i j = OfNat.ofNat 0 i j
apply det_eq_zero_of_column_eq_zero j'
case a.h.intro
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
j'' : n
⊢ updateColumn 0ᵀ j (Pi.single i 1) j'' j' = 0
case a.h.intro
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), updateColumn 0ᵀ j (Pi.single i 1) i_1 j' = 0
intro j''
no goals
case a.h.intro
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
j'' : n
⊢ updateColumn 0ᵀ j (Pi.single i 1) j'' j' = 0
simp [updateColumn_ne hj']