[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ IsLinearMap α (cramerMap A)
[PROOFSTEP]
constructor
[GOAL]
case map_add
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ ∀ (x y : n → α), cramerMap A (x + y) = cramerMap A x + cramerMap A y
[PROOFSTEP]
intros
[GOAL]
case map_smul
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ ∀ (c : α) (x : n → α), cramerMap A (c • x) = c • cramerMap A x
[PROOFSTEP]
intros
[GOAL]
case map_add
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b x✝ y✝ : n → α
⊢ cramerMap A (x✝ + y✝) = cramerMap A x✝ + cramerMap A y✝
[PROOFSTEP]
ext i
[GOAL]
case map_smul
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
c✝ : α
x✝ : n → α
⊢ cramerMap A (c✝ • x✝) = c✝ • cramerMap A x✝
[PROOFSTEP]
ext i
[GOAL]
case map_add.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b x✝ y✝ : n → α
i : n
⊢ cramerMap A (x✝ + y✝) i = (cramerMap A x✝ + cramerMap A y✝) i
[PROOFSTEP]
apply (cramerMap_is_linear A i).1
[GOAL]
case map_smul.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
c✝ : α
x✝ : n → α
i : n
⊢ cramerMap A (c✝ • x✝) i = (c✝ • cramerMap A x✝) i
[PROOFSTEP]
apply (cramerMap_is_linear A i).2
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
⊢ ↑(cramer Aᵀ) b i = det (updateRow A i b)
[PROOFSTEP]
rw [cramer_apply, updateColumn_transpose, det_transpose]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
⊢ ↑(cramer Aᵀ) (A i) = Pi.single i (det A)
[PROOFSTEP]
ext j
[GOAL]
case h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j : n
⊢ ↑(cramer Aᵀ) (A i) j = Pi.single i (det A) j
[PROOFSTEP]
rw [cramer_apply, Pi.single_apply]
[GOAL]
case h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j : n
⊢ det (updateColumn Aᵀ j (A i)) = if j = i then det A else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j : n
h : j = i
⊢ det (updateColumn Aᵀ j (A i)) = det A
[PROOFSTEP]
subst h
[GOAL]
case pos
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
j : n
⊢ det (updateColumn Aᵀ j (A j)) = det A
[PROOFSTEP]
simp only [updateColumn_transpose, det_transpose, updateRow_eq_self]
[GOAL]
case neg
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j : n
h : ¬j = i
⊢ det (updateColumn Aᵀ j (A i)) = 0
[PROOFSTEP]
rw [updateColumn_transpose, det_transpose]
[GOAL]
case neg
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j : n
h : ¬j = i
⊢ det (updateRow A j (A i)) = 0
[PROOFSTEP]
apply det_zero_of_row_eq h
[GOAL]
case neg
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j : n
h : ¬j = i
⊢ updateRow A j (A i) j = updateRow A j (A i) i
[PROOFSTEP]
rw [updateRow_self, updateRow_ne (Ne.symm h)]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ ↑(cramer A) b = Pi.single i (det A)
[PROOFSTEP]
rw [← transpose_transpose A, det_transpose]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ ↑(cramer Aᵀᵀ) b = Pi.single i (det Aᵀ)
[PROOFSTEP]
convert cramer_transpose_row_self Aᵀ i
[GOAL]
case h.e'_2.h.e'_6
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ b = Aᵀ i
[PROOFSTEP]
exact funext h
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ cramer 1 = 1
[PROOFSTEP]
refine LinearMap.pi_ext' (fun (i : n) => LinearMap.ext_ring (funext (fun (j : n) => ?_)))
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j : n
⊢ ↑(LinearMap.comp (cramer 1) (LinearMap.single i)) 1 j = ↑(LinearMap.comp 1 (LinearMap.single i)) 1 j
[PROOFSTEP]
convert congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j
[GOAL]
case h.e'_3.h.e'_1
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j : n
⊢ 1 = det 1
[PROOFSTEP]
simp
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j : n
⊢ ∀ (j : n), Pi.single i 1 j = OfNat.ofNat 1 j i
[PROOFSTEP]
intro j
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i j✝ j : n
⊢ Pi.single i 1 j = OfNat.ofNat 1 j i
[PROOFSTEP]
rw [Matrix.one_eq_pi_single, Pi.single_comm]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
A✝ : Matrix n n α
b✝ : n → α
inst✝ : Subsingleton n
A : Matrix n n α
b : n → α
i : n
⊢ ↑(cramer A) b i = b i
[PROOFSTEP]
rw [cramer_apply, det_eq_elem_of_subsingleton _ i, updateColumn_self]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
A : Matrix n n α
b : n → α
inst✝ : Nontrivial n
⊢ cramer 0 = 0
[PROOFSTEP]
ext i j
[GOAL]
case h.h.h
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
A : Matrix n n α
b : n → α
inst✝ : Nontrivial n
i j : n
⊢ ↑(LinearMap.comp (cramer 0) (LinearMap.single i)) 1 j = ↑(LinearMap.comp 0 (LinearMap.single i)) 1 j
[PROOFSTEP]
obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j
[GOAL]
case h.h.h.intro
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
A : Matrix n n α
b : n → α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ↑(LinearMap.comp (cramer 0) (LinearMap.single i)) 1 j = ↑(LinearMap.comp 0 (LinearMap.single i)) 1 j
[PROOFSTEP]
apply det_eq_zero_of_column_eq_zero j'
[GOAL]
case h.h.h.intro
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
A : Matrix n n α
b : n → α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), updateColumn 0 j (↑(LinearMap.single i) 1) i_1 j' = 0
[PROOFSTEP]
intro j''
[GOAL]
case h.h.h.intro
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
A : Matrix n n α
b : n → α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
j'' : n
⊢ updateColumn 0 j (↑(LinearMap.single i) 1) j'' j' = 0
[PROOFSTEP]
simp [updateColumn_ne hj']
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ Finset.sum s (fun x => ↑(cramer A) fun j => f j x) i = ↑(cramer A) (fun j => ∑ x in s, f j x) i
[PROOFSTEP]
rw [sum_cramer, cramer_apply, cramer_apply]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ det (updateColumn A i (∑ x in s, fun j => f j x)) = det (updateColumn A i fun j => ∑ x in s, f j x)
[PROOFSTEP]
simp only [updateColumn]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ det (↑of fun i_1 => Function.update (A i_1) i (Finset.sum s (fun x j => f j x) i_1)) =
    det (↑of fun i_1 => Function.update (A i_1) i (∑ x in s, f i_1 x))
[PROOFSTEP]
congr with j
[GOAL]
case e_M.h.e_6.h.h.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ Function.update (A j) i (Finset.sum s (fun x j => f j x) j) x✝ = Function.update (A j) i (∑ x in s, f j x) x✝
[PROOFSTEP]
congr
[GOAL]
case e_M.h.e_6.h.h.h.e_v
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ Finset.sum s (fun x j => f j x) j = ∑ x in s, f j x
[PROOFSTEP]
apply Finset.sum_apply
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A✝ : Matrix n n α
b✝ : n → α
A : Matrix m m α
e : n ≃ m
b : n → α
⊢ ↑(cramer (submatrix A ↑e ↑e)) b = ↑(cramer A) (b ∘ ↑e.symm) ∘ ↑e
[PROOFSTEP]
ext i
[GOAL]
case h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A✝ : Matrix n n α
b✝ : n → α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
⊢ ↑(cramer (submatrix A ↑e ↑e)) b i = (↑(cramer A) (b ∘ ↑e.symm) ∘ ↑e) i
[PROOFSTEP]
simp_rw [Function.comp_apply, cramer_apply, updateColumn_submatrix_equiv, det_submatrix_equiv_self e, Function.comp]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ adjugate A i j = det (updateRow A j (Pi.single i 1))
[PROOFSTEP]
rw [adjugate_def, of_apply, cramer_apply, updateColumn_transpose, det_transpose]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ (adjugate A)ᵀ = adjugate Aᵀ
[PROOFSTEP]
ext i j
[GOAL]
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 α
A : Matrix n n α
i j : n
⊢ (adjugate A)ᵀ i j = adjugate Aᵀ i j
[PROOFSTEP]
rw [transpose_apply, adjugate_apply, adjugate_apply, updateRow_transpose, det_transpose]
[GOAL]
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 α
A : Matrix n n α
i j : n
⊢ det (updateRow A i (Pi.single j 1)) = det (updateColumn A j (Pi.single i 1))
[PROOFSTEP]
rw [det_apply', det_apply']
[GOAL]
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 α
A : Matrix n n α
i j : n
⊢ ∑ σ : Perm n, ↑↑(↑sign σ) * ∏ i_1 : n, updateRow A i (Pi.single j 1) (↑σ i_1) i_1 =
    ∑ σ : Perm n, ↑↑(↑sign σ) * ∏ i_1 : n, updateColumn A j (Pi.single i 1) (↑σ i_1) i_1
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
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 α
A : Matrix n n α
i j : n
⊢ ∀ (x : Perm n),
    x ∈ univ →
      ↑↑(↑sign x) * ∏ i_1 : n, updateRow A i (Pi.single j 1) (↑x i_1) i_1 =
        ↑↑(↑sign x) * ∏ i_1 : n, updateColumn A j (Pi.single i 1) (↑x i_1) i_1
[PROOFSTEP]
intro σ _
[GOAL]
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 α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
⊢ ↑↑(↑sign σ) * ∏ i_1 : n, updateRow A i (Pi.single j 1) (↑σ i_1) i_1 =
    ↑↑(↑sign σ) * ∏ i_1 : n, updateColumn A j (Pi.single i 1) (↑σ i_1) i_1
[PROOFSTEP]
congr 1
[GOAL]
case a.h.e_a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
⊢ ∏ i_1 : n, updateRow A i (Pi.single j 1) (↑σ i_1) i_1 = ∏ i_1 : n, updateColumn A j (Pi.single i 1) (↑σ i_1) i_1
[PROOFSTEP]
by_cases i = σ j
[GOAL]
case a.h.e_a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
⊢ ∏ i_1 : n, updateRow A i (Pi.single j 1) (↑σ i_1) i_1 = ∏ i_1 : n, updateColumn A j (Pi.single i 1) (↑σ i_1) i_1
[PROOFSTEP]
by_cases i = σ j
[GOAL]
case pos
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = ↑σ j
⊢ ∏ i_1 : n, updateRow A i (Pi.single j 1) (↑σ i_1) i_1 = ∏ i_1 : n, updateColumn A j (Pi.single i 1) (↑σ i_1) i_1
[PROOFSTEP]
congr
[GOAL]
case pos.e_f
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = ↑σ j
⊢ (fun i_1 => updateRow A i (Pi.single j 1) (↑σ i_1) i_1) = fun i_1 => updateColumn A j (Pi.single i 1) (↑σ i_1) i_1
[PROOFSTEP]
ext j'
[GOAL]
case pos.e_f.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = ↑σ j
j' : n
⊢ updateRow A i (Pi.single j 1) (↑σ j') j' = updateColumn A j (Pi.single i 1) (↑σ j') j'
[PROOFSTEP]
subst h
[GOAL]
case pos.e_f.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
⊢ updateRow A (↑σ j) (Pi.single j 1) (↑σ j') j' = updateColumn A j (Pi.single (↑σ j) 1) (↑σ j') j'
[PROOFSTEP]
have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff
[GOAL]
case pos.e_f.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : ↑σ j' = ↑σ j ↔ j' = j
⊢ updateRow A (↑σ j) (Pi.single j 1) (↑σ j') j' = updateColumn A j (Pi.single (↑σ j) 1) (↑σ j') j'
[PROOFSTEP]
rw [updateRow_apply, updateColumn_apply]
[GOAL]
case pos.e_f.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : ↑σ j' = ↑σ j ↔ j' = j
⊢ (if ↑σ j' = ↑σ j then Pi.single j 1 j' else A (↑σ j') j') =
    if j' = j then Pi.single (↑σ j) 1 (↑σ j') else A (↑σ j') j'
[PROOFSTEP]
simp_rw [this]
[GOAL]
case pos.e_f.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : ↑σ j' = ↑σ j ↔ j' = j
⊢ (if j' = j then Pi.single j 1 j' else A (↑σ j') j') = if j' = j then Pi.single (↑σ j) 1 (↑σ j') else A (↑σ j') j'
[PROOFSTEP]
rw [← dite_eq_ite, ← dite_eq_ite]
[GOAL]
case pos.e_f.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : ↑σ j' = ↑σ j ↔ j' = j
⊢ (if x : j' = j then Pi.single j 1 j' else A (↑σ j') j') =
    if x : j' = j then Pi.single (↑σ j) 1 (↑σ j') else A (↑σ j') j'
[PROOFSTEP]
congr 1 with rfl
[GOAL]
case pos.e_f.h.e_t.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : ↑σ j' = ↑σ j' ↔ j' = j'
⊢ Pi.single j' 1 j' = Pi.single (↑σ j') 1 (↑σ j')
[PROOFSTEP]
rw [Pi.single_eq_same, Pi.single_eq_same]
[GOAL]
case neg
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = ↑σ j
⊢ ∏ i_1 : n, updateRow A i (Pi.single j 1) (↑σ i_1) i_1 = ∏ i_1 : n, updateColumn A j (Pi.single i 1) (↑σ i_1) i_1
[PROOFSTEP]
have : (∏ j' : n, updateColumn A j (Pi.single i 1) (σ j') j') = 0 :=
  by
  apply prod_eq_zero (mem_univ j)
  rw [updateColumn_self, Pi.single_eq_of_ne' h]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = ↑σ j
⊢ ∏ j' : n, updateColumn A j (Pi.single i 1) (↑σ j') j' = 0
[PROOFSTEP]
apply prod_eq_zero (mem_univ j)
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = ↑σ j
⊢ updateColumn A j (Pi.single i 1) (↑σ j) j = 0
[PROOFSTEP]
rw [updateColumn_self, Pi.single_eq_of_ne' h]
[GOAL]
case neg
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = ↑σ j
this : ∏ j' : n, updateColumn A j (Pi.single i 1) (↑σ j') j' = 0
⊢ ∏ i_1 : n, updateRow A i (Pi.single j 1) (↑σ i_1) i_1 = ∏ i_1 : n, updateColumn A j (Pi.single i 1) (↑σ i_1) i_1
[PROOFSTEP]
rw [this]
[GOAL]
case neg
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = ↑σ j
this : ∏ j' : n, updateColumn A j (Pi.single i 1) (↑σ j') j' = 0
⊢ ∏ i_1 : n, updateRow A i (Pi.single j 1) (↑σ i_1) i_1 = 0
[PROOFSTEP]
apply prod_eq_zero (mem_univ (σ⁻¹ i))
[GOAL]
case neg
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = ↑σ j
this : ∏ j' : n, updateColumn A j (Pi.single i 1) (↑σ j') j' = 0
⊢ updateRow A i (Pi.single j 1) (↑σ (↑σ⁻¹ i)) (↑σ⁻¹ i) = 0
[PROOFSTEP]
erw [apply_symm_apply σ i, updateRow_self]
[GOAL]
case neg
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = ↑σ j
this : ∏ j' : n, updateColumn A j (Pi.single i 1) (↑σ j') j' = 0
⊢ Pi.single j 1 (↑σ⁻¹ i) = 0
[PROOFSTEP]
apply Pi.single_eq_of_ne
[GOAL]
case neg.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = ↑σ j
this : ∏ j' : n, updateColumn A j (Pi.single i 1) (↑σ j') j' = 0
⊢ ↑σ⁻¹ i ≠ j
[PROOFSTEP]
intro h'
[GOAL]
case neg.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = ↑σ j
this : ∏ j' : n, updateColumn A j (Pi.single i 1) (↑σ j') j' = 0
h' : ↑σ⁻¹ i = j
⊢ False
[PROOFSTEP]
exact h ((symm_apply_eq σ).mp h')
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
⊢ adjugate (submatrix A ↑e ↑e) = submatrix (adjugate A) ↑e ↑e
[PROOFSTEP]
ext i j
[GOAL]
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 α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ adjugate (submatrix A ↑e ↑e) i j = submatrix (adjugate A) (↑e) (↑e) i j
[PROOFSTEP]
rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e, updateRow_submatrix_equiv]
  -- Porting note: added
[GOAL]
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 α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ det (submatrix (updateRow A (↑e j) fun j => Pi.single i 1 (↑e.symm j)) ↑e ↑e) =
    det (submatrix (updateRow A (↑e j) (Pi.single (↑e i) 1)) ↑e ↑e)
[PROOFSTEP]
suffices (fun j => Pi.single i 1 (e.symm j)) = Pi.single (e i) 1 by erw [this]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
this : (fun j => Pi.single i 1 (↑e.symm j)) = Pi.single (↑e i) 1
⊢ det (submatrix (updateRow A (↑e j) fun j => Pi.single i 1 (↑e.symm j)) ↑e ↑e) =
    det (submatrix (updateRow A (↑e j) (Pi.single (↑e i) 1)) ↑e ↑e)
[PROOFSTEP]
erw [this]
[GOAL]
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 α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ (fun j => Pi.single i 1 (↑e.symm j)) = Pi.single (↑e i) 1
[PROOFSTEP]
exact Function.update_comp_equiv _ e.symm _ _
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ ↑(cramer A) b = mulVec (adjugate A) b
[PROOFSTEP]
nth_rw 2 [← A.transpose_transpose]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ ↑(cramer A) b = mulVec (adjugate Aᵀᵀ) b
[PROOFSTEP]
rw [← adjugate_transpose, adjugate_def]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ ↑(cramer A) b = mulVec (↑of fun i => ↑(cramer Aᵀᵀ) (Pi.single i 1))ᵀ b
[PROOFSTEP]
have : b = ∑ i, b i • Pi.single i 1 := by
  refine' (pi_eq_sum_univ b).trans _
  congr with j
  simp [Pi.single_apply, eq_comm, Pi.smul_apply (b j)]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ b = ∑ i : n, b i • Pi.single i 1
[PROOFSTEP]
refine' (pi_eq_sum_univ b).trans _
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ (∑ i : n, b i • fun j => if i = j then 1 else 0) = ∑ i : n, b i • Pi.single i 1
[PROOFSTEP]
congr with j
[GOAL]
case e_f.h.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
j x✝ : n
⊢ (b j • fun j_1 => if j = j_1 then 1 else 0) x✝ = (b j • Pi.single j 1) x✝
[PROOFSTEP]
simp [Pi.single_apply, eq_comm, Pi.smul_apply (b j)]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
⊢ ↑(cramer A) b = mulVec (↑of fun i => ↑(cramer Aᵀᵀ) (Pi.single i 1))ᵀ b
[PROOFSTEP]
conv_lhs => rw [this]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
| ↑(cramer A) b
[PROOFSTEP]
rw [this]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
| ↑(cramer A) b
[PROOFSTEP]
rw [this]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
| ↑(cramer A) b
[PROOFSTEP]
rw [this]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
⊢ ↑(cramer A) (∑ i : n, b i • Pi.single i 1) = mulVec (↑of fun i => ↑(cramer Aᵀᵀ) (Pi.single i 1))ᵀ b
[PROOFSTEP]
ext k
[GOAL]
case h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
k : n
⊢ ↑(cramer A) (∑ i : n, b i • Pi.single i 1) k = mulVec (↑of fun i => ↑(cramer Aᵀᵀ) (Pi.single i 1))ᵀ b k
[PROOFSTEP]
simp [mulVec, dotProduct, mul_comm]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i j k : n
⊢ A i k * adjugate A k j = ↑(cramer Aᵀ) (Pi.single k (A i k)) j
[PROOFSTEP]
erw [← smul_eq_mul, adjugate, of_apply, ← Pi.smul_apply, ← LinearMap.map_smul, ← Pi.single_smul', smul_eq_mul, mul_one]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ A * adjugate A = det A • 1
[PROOFSTEP]
ext i j
[GOAL]
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 α
A : Matrix n n α
i j : n
⊢ (A * adjugate A) i j = (det A • 1) i j
[PROOFSTEP]
rw [mul_apply, Pi.smul_apply, Pi.smul_apply, one_apply, smul_eq_mul, mul_boole]
[GOAL]
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 α
A : Matrix n n α
i j : n
⊢ ∑ j_1 : n, A i j_1 * adjugate A j_1 j = if i = j then det A else 0
[PROOFSTEP]
simp [mul_adjugate_apply, sum_cramer_apply, cramer_transpose_row_self, Pi.single_apply, eq_comm]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ adjugate A * A = (Aᵀ * adjugate Aᵀ)ᵀ
[PROOFSTEP]
rw [← adjugate_transpose, ← transpose_mul, transpose_transpose]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ (Aᵀ * adjugate Aᵀ)ᵀ = det A • 1
[PROOFSTEP]
rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
r : α
A : Matrix n n α
⊢ adjugate (r • A) = r ^ (Fintype.card n - 1) • adjugate A
[PROOFSTEP]
rw [adjugate, adjugate, transpose_smul, cramer_smul]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
r : α
A : Matrix n n α
⊢ (↑of fun i => ↑(r ^ (Fintype.card n - 1) • cramer Aᵀ) (Pi.single i 1)) =
    r ^ (Fintype.card n - 1) • ↑of fun i => ↑(cramer Aᵀ) (Pi.single i 1)
[PROOFSTEP]
rfl
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ mulVec A (↑(cramer A) b) = det A • b
[PROOFSTEP]
rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec_assoc, one_mulVec]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
⊢ adjugate A = 1
[PROOFSTEP]
ext i j
[GOAL]
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✝ : Subsingleton n
A : Matrix n n α
i j : n
⊢ adjugate A i j = OfNat.ofNat 1 i j
[PROOFSTEP]
simp [Subsingleton.elim i j, adjugate_apply, det_eq_elem_of_subsingleton _ i]
[GOAL]
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
[PROOFSTEP]
ext i j
[GOAL]
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
[PROOFSTEP]
obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j
[GOAL]
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
[PROOFSTEP]
apply det_eq_zero_of_column_eq_zero j'
[GOAL]
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
[PROOFSTEP]
intro j''
[GOAL]
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
[PROOFSTEP]
simp [updateColumn_ne hj']
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
⊢ adjugate 1 = 1
[PROOFSTEP]
ext
[GOAL]
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 α
i✝ x✝ : n
⊢ adjugate 1 i✝ x✝ = OfNat.ofNat 1 i✝ x✝
[PROOFSTEP]
simp [adjugate_def, Matrix.one_apply, Pi.single_apply, eq_comm]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
⊢ adjugate (diagonal v) = diagonal fun i => ∏ j in Finset.erase univ i, v j
[PROOFSTEP]
ext i j
[GOAL]
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 α
v : n → α
i j : n
⊢ adjugate (diagonal v) i j = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i j
[PROOFSTEP]
simp only [adjugate_def, cramer_apply, diagonal_transpose, of_apply]
[GOAL]
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 α
v : n → α
i j : n
⊢ det (updateColumn (diagonal v) j (Pi.single i 1)) = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i j
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case a.h.inl
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i : n
⊢ det (updateColumn (diagonal v) i (Pi.single i 1)) = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i i
[PROOFSTEP]
rw [diagonal_apply_eq, diagonal_updateColumn_single, det_diagonal, prod_update_of_mem (Finset.mem_univ _),
  sdiff_singleton_eq_erase, one_mul]
[GOAL]
case a.h.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ det (updateColumn (diagonal v) j (Pi.single i 1)) = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i j
[PROOFSTEP]
rw [diagonal_apply_ne _ hij]
[GOAL]
case a.h.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ det (updateColumn (diagonal v) j (Pi.single i 1)) = 0
[PROOFSTEP]
refine' det_eq_zero_of_row_eq_zero j fun k => _
[GOAL]
case a.h.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
⊢ updateColumn (diagonal v) j (Pi.single i 1) j k = 0
[PROOFSTEP]
obtain rfl | hjk := eq_or_ne k j
[GOAL]
case a.h.inr.inl
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i k : n
hij : i ≠ k
⊢ updateColumn (diagonal v) k (Pi.single i 1) k k = 0
[PROOFSTEP]
rw [updateColumn_self, Pi.single_eq_of_ne' hij]
[GOAL]
case a.h.inr.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
hjk : k ≠ j
⊢ updateColumn (diagonal v) j (Pi.single i 1) j k = 0
[PROOFSTEP]
rw [updateColumn_ne hjk, diagonal_apply_ne' _ hjk]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : CommRing α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
⊢ ↑(RingHom.mapMatrix f) (adjugate M) = adjugate (↑(RingHom.mapMatrix f) M)
[PROOFSTEP]
ext i k
[GOAL]
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 α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ ↑(RingHom.mapMatrix f) (adjugate M) i k = adjugate (↑(RingHom.mapMatrix f) M) i k
[PROOFSTEP]
have : Pi.single i (1 : S) = f ∘ Pi.single i 1 := by
  rw [← f.map_one]
  exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : CommRing α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i 1 = ↑f ∘ Pi.single i 1
[PROOFSTEP]
rw [← f.map_one]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : CommRing α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i (↑f 1) = ↑f ∘ Pi.single i 1
[PROOFSTEP]
exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)
[GOAL]
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 α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ↑f ∘ Pi.single i 1
⊢ ↑(RingHom.mapMatrix f) (adjugate M) i k = adjugate (↑(RingHom.mapMatrix f) M) i k
[PROOFSTEP]
rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ← map_updateRow, ←
  RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ det (adjugate A) = det A ^ (Fintype.card n - 1)
[PROOFSTEP]
cases' (Fintype.card n).eq_zero_or_pos with h_card h_card
[GOAL]
case inl
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n = 0
⊢ det (adjugate A) = det A ^ (Fintype.card n - 1)
[PROOFSTEP]
haveI : IsEmpty n := Fintype.card_eq_zero_iff.mp h_card
[GOAL]
case inl
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n = 0
this : IsEmpty n
⊢ det (adjugate A) = det A ^ (Fintype.card n - 1)
[PROOFSTEP]
rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_one]
[GOAL]
case inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n > 0
⊢ det (adjugate A) = det A ^ (Fintype.card n - 1)
[PROOFSTEP]
replace h_card := tsub_add_cancel_of_le h_card.nat_succ_le
[GOAL]
case inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
⊢ det (adjugate A) = det A ^ (Fintype.card n - 1)
[PROOFSTEP]
let A' := mvPolynomialX n n ℤ
[GOAL]
case inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ det (adjugate A) = det A ^ (Fintype.card n - 1)
[PROOFSTEP]
suffices A'.adjugate.det = A'.det ^ (Fintype.card n - 1) by
  rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ← AlgHom.map_det, ← AlgHom.map_pow,
    this]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : det (adjugate A') = det A' ^ (Fintype.card n - 1)
⊢ det (adjugate A) = det A ^ (Fintype.card n - 1)
[PROOFSTEP]
rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ← AlgHom.map_det, ← AlgHom.map_pow,
  this]
[GOAL]
case inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ det (adjugate A') = det A' ^ (Fintype.card n - 1)
[PROOFSTEP]
apply mul_left_cancel₀ (show A'.det ≠ 0 from det_mvPolynomialX_ne_zero n ℤ)
[GOAL]
case inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ det A' * det (adjugate A') = det A' * det A' ^ (Fintype.card n - 1)
[PROOFSTEP]
calc
  A'.det * A'.adjugate.det = (A' * adjugate A').det := (det_mul _ _).symm
  _ = A'.det ^ Fintype.card n := by rw [mul_adjugate, det_smul, det_one, mul_one]
  _ = A'.det * A'.det ^ (Fintype.card n - 1) := by rw [← pow_succ, h_card]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ det (A' * adjugate A') = det A' ^ Fintype.card n
[PROOFSTEP]
rw [mul_adjugate, det_smul, det_one, mul_one]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ det A' ^ Fintype.card n = det A' * det A' ^ (Fintype.card n - 1)
[PROOFSTEP]
rw [← pow_succ, h_card]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ adjugate A = ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]]
[PROOFSTEP]
ext i j
[GOAL]
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 α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ adjugate A i j = ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] i j
[PROOFSTEP]
rw [adjugate_apply, det_fin_two]
[GOAL]
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 α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ updateRow A j (Pi.single i 1) 0 0 * updateRow A j (Pi.single i 1) 1 1 -
      updateRow A j (Pi.single i 1) 0 1 * updateRow A j (Pi.single i 1) 1 0 =
    ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ updateRow A j (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 0 0 *
        updateRow A j (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 1 1 -
      updateRow A j (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 0 1 *
        updateRow A j (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 1 0 =
    ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ updateRow A j (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 0 0 *
        updateRow A j (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 1 1 -
      updateRow A j (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 0 1 *
        updateRow A j (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 1 0 =
    ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ updateRow A { val := 0, isLt := (_ : 0 < 2) } (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 0 0 *
        updateRow A { val := 0, isLt := (_ : 0 < 2) } (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 1 1 -
      updateRow A { val := 0, isLt := (_ : 0 < 2) } (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 0 1 *
        updateRow A { val := 0, isLt := (_ : 0 < 2) } (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 1 0 =
    ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [one_mul, Fin.one_eq_zero_iff, Pi.single_eq_same, mul_zero, sub_zero, Pi.single_eq_of_ne, Ne.def, not_false_iff,
  updateRow_self, updateRow_ne, cons_val_zero, of_apply, Nat.succ_succ_ne_one, Pi.single_eq_of_ne, updateRow_self,
  Pi.single_eq_of_ne, Ne.def, Fin.zero_eq_one_iff, Nat.succ_succ_ne_one, not_false_iff, updateRow_ne,
  Fin.one_eq_zero_iff, zero_mul, Pi.single_eq_same, one_mul, zero_sub, of_apply, cons_val', cons_val_fin_one,
  cons_val_one, head_fin_const, neg_inj, eq_self_iff_true, cons_val_zero, head_cons, mul_one]
[GOAL]
case a.h.head.tail.head
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ updateRow A { val := 1, isLt := (_ : (fun a => a < 2) 1) } (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 0 0 *
        updateRow A { val := 1, isLt := (_ : (fun a => a < 2) 1) } (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 1 1 -
      updateRow A { val := 1, isLt := (_ : (fun a => a < 2) 1) } (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 0 1 *
        updateRow A { val := 1, isLt := (_ : (fun a => a < 2) 1) } (Pi.single { val := 0, isLt := (_ : 0 < 2) } 1) 1 0 =
    ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [one_mul, Fin.one_eq_zero_iff, Pi.single_eq_same, mul_zero, sub_zero, Pi.single_eq_of_ne, Ne.def, not_false_iff,
  updateRow_self, updateRow_ne, cons_val_zero, of_apply, Nat.succ_succ_ne_one, Pi.single_eq_of_ne, updateRow_self,
  Pi.single_eq_of_ne, Ne.def, Fin.zero_eq_one_iff, Nat.succ_succ_ne_one, not_false_iff, updateRow_ne,
  Fin.one_eq_zero_iff, zero_mul, Pi.single_eq_same, one_mul, zero_sub, of_apply, cons_val', cons_val_fin_one,
  cons_val_one, head_fin_const, neg_inj, eq_self_iff_true, cons_val_zero, head_cons, mul_one]
[GOAL]
case a.h.tail.head.head
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ updateRow A { val := 0, isLt := (_ : 0 < 2) } (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 0 0 *
        updateRow A { val := 0, isLt := (_ : 0 < 2) } (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 1 1 -
      updateRow A { val := 0, isLt := (_ : 0 < 2) } (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 0 1 *
        updateRow A { val := 0, isLt := (_ : 0 < 2) } (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 1 0 =
    ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [one_mul, Fin.one_eq_zero_iff, Pi.single_eq_same, mul_zero, sub_zero, Pi.single_eq_of_ne, Ne.def, not_false_iff,
  updateRow_self, updateRow_ne, cons_val_zero, of_apply, Nat.succ_succ_ne_one, Pi.single_eq_of_ne, updateRow_self,
  Pi.single_eq_of_ne, Ne.def, Fin.zero_eq_one_iff, Nat.succ_succ_ne_one, not_false_iff, updateRow_ne,
  Fin.one_eq_zero_iff, zero_mul, Pi.single_eq_same, one_mul, zero_sub, of_apply, cons_val', cons_val_fin_one,
  cons_val_one, head_fin_const, neg_inj, eq_self_iff_true, cons_val_zero, head_cons, mul_one]
[GOAL]
case a.h.tail.head.tail.head
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ updateRow A { val := 1, isLt := (_ : (fun a => a < 2) 1) }
          (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 0 0 *
        updateRow A { val := 1, isLt := (_ : (fun a => a < 2) 1) }
          (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 1 1 -
      updateRow A { val := 1, isLt := (_ : (fun a => a < 2) 1) }
          (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 0 1 *
        updateRow A { val := 1, isLt := (_ : (fun a => a < 2) 1) }
          (Pi.single { val := 1, isLt := (_ : (fun a => a < 2) 1) } 1) 1 0 =
    ↑of ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [one_mul, Fin.one_eq_zero_iff, Pi.single_eq_same, mul_zero, sub_zero, Pi.single_eq_of_ne, Ne.def, not_false_iff,
  updateRow_self, updateRow_ne, cons_val_zero, of_apply, Nat.succ_succ_ne_one, Pi.single_eq_of_ne, updateRow_self,
  Pi.single_eq_of_ne, Ne.def, Fin.zero_eq_one_iff, Nat.succ_succ_ne_one, not_false_iff, updateRow_ne,
  Fin.one_eq_zero_iff, zero_mul, Pi.single_eq_same, one_mul, zero_sub, of_apply, cons_val', cons_val_fin_one,
  cons_val_one, head_fin_const, neg_inj, eq_self_iff_true, cons_val_zero, head_cons, mul_one]
[GOAL]
m : Type u
n✝ : Type v
α : Type w
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) α
i j : Fin (Nat.succ n)
⊢ adjugate A i j = (-1) ^ (↑j + ↑i) * det (submatrix A (Fin.succAbove j) (Fin.succAbove i))
[PROOFSTEP]
simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]
[GOAL]
m : Type u
n✝ : Type v
α : Type w
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) α
i j : Fin (Nat.succ n)
⊢ ∑ x : Fin (Nat.succ n), (-1) ^ (↑j + ↑x) * Pi.single i 1 x * det (submatrix A (Fin.succAbove j) (Fin.succAbove x)) =
    (-1) ^ (↑j + ↑i) * det (submatrix A (Fin.succAbove j) (Fin.succAbove i))
[PROOFSTEP]
rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]
[GOAL]
m : Type u
n✝ : Type v
α : Type w
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) α
i j h : Fin (Nat.succ n)
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * det (submatrix A (Fin.succAbove j) (Fin.succAbove h)) = 0
[PROOFSTEP]
rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
⊢ det A = ∑ j : n, A i j * adjugate A j i
[PROOFSTEP]
haveI : Nonempty n := ⟨i⟩
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
⊢ det A = ∑ j : n, A i j * adjugate A j i
[PROOFSTEP]
obtain ⟨n', hn'⟩ := Nat.exists_eq_succ_of_ne_zero (Fintype.card_ne_zero : Fintype.card n ≠ 0)
[GOAL]
case intro
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
⊢ det A = ∑ j : n, A i j * adjugate A j i
[PROOFSTEP]
obtain ⟨e⟩ := Fintype.truncEquivFinOfCardEq hn'
[GOAL]
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
⊢ det A = ∑ j : n, A i j * adjugate A j i
[PROOFSTEP]
let A' := reindex e e A
[GOAL]
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
⊢ det A = ∑ j : n, A i j * adjugate A j i
[PROOFSTEP]
suffices det A' = ∑ j : Fin n'.succ, A' (e i) j * adjugate A' j (e i)
  by
  simp_rw [det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp, Equiv.symm_apply_apply] at
    this 
  exact this
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
this : det A' = ∑ j : Fin (Nat.succ n'), A' (↑e i) j * adjugate A' j (↑e i)
⊢ det A = ∑ j : n, A i j * adjugate A j i
[PROOFSTEP]
simp_rw [det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp, Equiv.symm_apply_apply] at
  this 
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
this : det A = ∑ x : n, A i x * adjugate A x i
⊢ det A = ∑ j : n, A i j * adjugate A j i
[PROOFSTEP]
exact this
[GOAL]
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
⊢ det A' = ∑ j : Fin (Nat.succ n'), A' (↑e i) j * adjugate A' j (↑e i)
[PROOFSTEP]
rw [det_succ_row A' (e i)]
[GOAL]
case intro.mk
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = Nat.succ n'
x✝ : Trunc (n ≃ Fin (Nat.succ n'))
e : n ≃ Fin (Nat.succ n')
A' : (fun x => Matrix (Fin (Nat.succ n')) (Fin (Nat.succ n')) α) A := ↑(reindex e e) A
⊢ ∑ j : Fin (Nat.succ n'),
      (-1) ^ (↑(↑e i) + ↑j) * A' (↑e i) j * det (submatrix A' (Fin.succAbove (↑e i)) (Fin.succAbove j)) =
    ∑ j : Fin (Nat.succ n'), A' (↑e i) j * adjugate A' j (↑e i)
[PROOFSTEP]
simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
j : n
⊢ det A = ∑ i : n, A i j * adjugate A j i
[PROOFSTEP]
simpa only [det_transpose, ← adjugate_transpose] using det_eq_sum_mul_adjugate_row Aᵀ j
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ (adjugate A)ᴴ = adjugate Aᴴ
[PROOFSTEP]
dsimp only [conjTranspose]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ map (adjugate A)ᵀ star = adjugate (map Aᵀ star)
[PROOFSTEP]
have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) := (starRingEnd α).map_adjugate Aᵀ
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
this : map (adjugate Aᵀ) star = adjugate (map Aᵀ star)
⊢ map (adjugate A)ᵀ star = adjugate (map Aᵀ star)
[PROOFSTEP]
rw [A.adjugate_transpose, this]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
⊢ IsRegular A
[PROOFSTEP]
constructor
[GOAL]
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
⊢ IsLeftRegular A
[PROOFSTEP]
intro B C h
[GOAL]
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : (fun x => A * x) B = (fun x => A * x) C
⊢ B = C
[PROOFSTEP]
refine' hA.matrix _
[GOAL]
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : (fun x => A * x) B = (fun x => A * x) C
⊢ (fun x => det A • x) B = (fun x => det A • x) C
[PROOFSTEP]
simp only at h ⊢
[GOAL]
case left
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : A * B = A * C
⊢ det A • B = det A • C
[PROOFSTEP]
rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ← adjugate_mul, Matrix.mul_assoc,
  Matrix.mul_assoc, h]
[GOAL]
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
⊢ IsRightRegular A
[PROOFSTEP]
intro B C (h : B * A = C * A)
[GOAL]
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : B * A = C * A
⊢ B = C
[PROOFSTEP]
refine' hA.matrix _
[GOAL]
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : B * A = C * A
⊢ (fun x => det A • x) B = (fun x => det A • x) C
[PROOFSTEP]
simp only
[GOAL]
case right
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular (det A)
B C : Matrix n n α
h : B * A = C * A
⊢ det A • B = det A • C
[PROOFSTEP]
rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ← mul_adjugate, ← Matrix.mul_assoc, ←
  Matrix.mul_assoc, h]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
⊢ adjugate (A * B) = adjugate B * adjugate A
[PROOFSTEP]
have hAB : IsLeftRegular (A * B).det := by
  rw [det_mul]
  exact hA.mul hB
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
⊢ IsLeftRegular (det (A * B))
[PROOFSTEP]
rw [det_mul]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
⊢ IsLeftRegular (det A * det B)
[PROOFSTEP]
exact hA.mul hB
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
hAB : IsLeftRegular (det (A * B))
⊢ adjugate (A * B) = adjugate B * adjugate A
[PROOFSTEP]
refine' (isRegular_of_isLeftRegular_det hAB).left _
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
hAB : IsLeftRegular (det (A * B))
⊢ (fun x => A * B * x) (adjugate (A * B)) = (fun x => A * B * x) (adjugate B * adjugate A)
[PROOFSTEP]
simp only
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
hAB : IsLeftRegular (det (A * B))
⊢ A * B * adjugate (A * B) = A * B * (adjugate B * adjugate A)
[PROOFSTEP]
rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate, smul_mul, Matrix.one_mul, mul_smul,
  mul_adjugate, smul_smul, mul_comm, ← det_mul]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
⊢ adjugate (A * B) = adjugate B * adjugate A
[PROOFSTEP]
let g : Matrix n n α → Matrix n n α[X] := fun M => M.map Polynomial.C + (Polynomial.X : α[X]) • (1 : Matrix n n α[X])
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
⊢ adjugate (A * B) = adjugate B * adjugate A
[PROOFSTEP]
let f' : Matrix n n α[X] →+* Matrix n n α := (Polynomial.evalRingHom 0).mapMatrix
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
⊢ adjugate (A * B) = adjugate B * adjugate A
[PROOFSTEP]
have f'_inv : ∀ M, f' (g M) = M := by
  intro
  ext
  simp
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
⊢ ∀ (M : Matrix n n α), ↑f' (g M) = M
[PROOFSTEP]
intro
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
M✝ : Matrix n n α
⊢ ↑f' (g M✝) = M✝
[PROOFSTEP]
ext
[GOAL]
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 α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
M✝ : Matrix n n α
i✝ x✝ : n
⊢ ↑f' (g M✝) i✝ x✝ = M✝ i✝ x✝
[PROOFSTEP]
simp
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
⊢ adjugate (A * B) = adjugate B * adjugate A
[PROOFSTEP]
have f'_adj : ∀ M : Matrix n n α, f' (adjugate (g M)) = adjugate M :=
  by
  intro
  rw [RingHom.map_adjugate, f'_inv]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
⊢ ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
[PROOFSTEP]
intro
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
M✝ : Matrix n n α
⊢ ↑f' (adjugate (g M✝)) = adjugate M✝
[PROOFSTEP]
rw [RingHom.map_adjugate, f'_inv]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
⊢ adjugate (A * B) = adjugate B * adjugate A
[PROOFSTEP]
have f'_g_mul : ∀ M N : Matrix n n α, f' (g M * g N) = M * N :=
  by
  intros M N
  rw [RingHom.map_mul, f'_inv, f'_inv]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
⊢ ∀ (M N : Matrix n n α), ↑f' (g M * g N) = M * N
[PROOFSTEP]
intros M N
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
M N : Matrix n n α
⊢ ↑f' (g M * g N) = M * N
[PROOFSTEP]
rw [RingHom.map_mul, f'_inv, f'_inv]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M * g N) = M * N
⊢ adjugate (A * B) = adjugate B * adjugate A
[PROOFSTEP]
have hu : ∀ M : Matrix n n α, IsRegular (g M).det := by
  intro M
  refine' Polynomial.Monic.isRegular _
  simp only [Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M * g N) = M * N
⊢ ∀ (M : Matrix n n α), IsRegular (det (g M))
[PROOFSTEP]
intro M
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M * g N) = M * N
M : Matrix n n α
⊢ IsRegular (det (g M))
[PROOFSTEP]
refine' Polynomial.Monic.isRegular _
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M * g N) = M * N
M : Matrix n n α
⊢ Monic (det (g M))
[PROOFSTEP]
simp only [Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (det (g M))
⊢ adjugate (A * B) = adjugate B * adjugate A
[PROOFSTEP]
rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ← adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left,
  RingHom.map_adjugate, RingHom.map_adjugate, f'_inv, f'_g_mul]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
⊢ adjugate (A ^ k) = adjugate A ^ k
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ adjugate (A ^ Nat.zero) = adjugate A ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
IH : adjugate (A ^ k) = adjugate A ^ k
⊢ adjugate (A ^ Nat.succ k) = adjugate A ^ Nat.succ k
[PROOFSTEP]
rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A
[PROOFSTEP]
have : A * (A.adjugate * A.adjugate.adjugate) = A * (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by
  rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
⊢ A * (adjugate A * adjugate (adjugate A)) = A * det A ^ (Fintype.card n - 1) • 1
[PROOFSTEP]
rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
this : A * (adjugate A * adjugate (adjugate A)) = A * det A ^ (Fintype.card n - 1) • 1
⊢ det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A
[PROOFSTEP]
rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul, Matrix.one_mul] at this 
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
⊢ adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A
[PROOFSTEP]
cases' h_card : Fintype.card n with n'
[GOAL]
case zero
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
h_card : Fintype.card n = Nat.zero
⊢ adjugate (adjugate A) = det A ^ (Nat.zero - 2) • A
[PROOFSTEP]
haveI : IsEmpty n := Fintype.card_eq_zero_iff.mp h_card
[GOAL]
case zero
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
h_card : Fintype.card n = Nat.zero
this : IsEmpty n
⊢ adjugate (adjugate A) = det A ^ (Nat.zero - 2) • A
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n' : ℕ
h_card : Fintype.card n = Nat.succ n'
⊢ adjugate (adjugate A) = det A ^ (Nat.succ n' - 2) • A
[PROOFSTEP]
cases n'
[GOAL]
case succ.zero
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
h_card : Fintype.card n = Nat.succ Nat.zero
⊢ adjugate (adjugate A) = det A ^ (Nat.succ Nat.zero - 2) • A
[PROOFSTEP]
exact (h h_card).elim
[GOAL]
case succ.succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
⊢ adjugate (adjugate A) = det A ^ (Nat.succ (Nat.succ n✝) - 2) • A
[PROOFSTEP]
rw [← h_card]
  -- express `A` as an evaluation of a polynomial in n^2 variables, and solve in the polynomial ring
    -- where `A'.det` is non-zero.
[GOAL]
case succ.succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
⊢ adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A
[PROOFSTEP]
let A' := mvPolynomialX n n ℤ
[GOAL]
case succ.succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A
[PROOFSTEP]
suffices adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A' by
  rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this, ← AlgHom.map_det, ←
    AlgHom.map_pow, AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (_root_.map_mul _)]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A'
⊢ adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A
[PROOFSTEP]
rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this, ← AlgHom.map_det, ←
  AlgHom.map_pow, AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (_root_.map_mul _)]
[GOAL]
case succ.succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A'
[PROOFSTEP]
have h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1 := by simp [h_card]
[GOAL]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ Fintype.card n - 2 + 1 = Fintype.card n - 1
[PROOFSTEP]
simp [h_card]
[GOAL]
case succ.succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
⊢ adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A'
[PROOFSTEP]
have is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A') := fun x y =>
  mul_left_cancel₀ (det_mvPolynomialX_ne_zero n ℤ)
[GOAL]
case succ.succ
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A')
⊢ adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A'
[PROOFSTEP]
apply is_reg.matrix
[GOAL]
case succ.succ.a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A')
⊢ (fun x => det A' • x) (adjugate (adjugate A')) = (fun x => det A' • x) (det A' ^ (Fintype.card n - 2) • A')
[PROOFSTEP]
simp only
[GOAL]
case succ.succ.a
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = Nat.succ (Nat.succ n✝)
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A')
⊢ det (mvPolynomialX n n ℤ) • adjugate (adjugate (mvPolynomialX n n ℤ)) =
    det (mvPolynomialX n n ℤ) • det (mvPolynomialX n n ℤ) ^ (Fintype.card n - 2) • mvPolynomialX n n ℤ
[PROOFSTEP]
rw [smul_smul, ← pow_succ, h_card', det_smul_adjugate_adjugate]
