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
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
refine LinearMap.pi_ext' (fun (i : n) => LinearMap.ext_ring (funext (fun (j : n) => ?_)))
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

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
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
convert congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j
no goals
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
simp
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
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
intro j
no goals
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
rw [Matrix.one_eq_pi_single, Pi.single_comm]