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
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
nth_rw 2 [← A.transpose_transpose]
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
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
rw [← adjugate_transpose, adjugate_def]
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
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
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)]
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
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
conv_lhs =>
  rw [this]
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
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
ext k
no goals
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
simp [mulVec, dotProduct, mul_comm]
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
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
refine' (pi_eq_sum_univ b).trans _
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✝
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
congr with j
no goals
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✝
simp [Pi.single_apply, eq_comm, Pi.smul_apply (b j)]