m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ mulVec M w = 0
⊢ v = 0
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
⊢ Nondegenerate M
intro v hv
case h
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ mulVec M w = 0
i : m
⊢ v i = OfNat.ofNat 0 i
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ mulVec M w = 0
⊢ v = 0
ext i
case h
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i = OfNat.ofNat 0 i
case h
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ mulVec M w = 0
i : m
⊢ v i = OfNat.ofNat 0 i
specialize hv (M.cramer (Pi.single i 1))
case h
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = 0
case h
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i = OfNat.ofNat 0 i
refine' (mul_eq_zero.mp _).resolve_right hM
case h.e'_2
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1))
case h
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = 0
convert hv
case h.e'_2
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = Finset.sum Finset.univ fun x => v x * (det M * Pi.single i 1 x)
case h.e'_2
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1))
simp only [mulVec_cramer M (Pi.single i 1), dotProduct, Pi.smul_apply, smul_eq_mul]
case h.e'_2.h₀
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ i → v b * (det M * Pi.single i 1 b) = 0

case h.e'_2.h₁
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ ¬i ∈ Finset.univ → v i * (det M * Pi.single i 1 i) = 0
case h.e'_2
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = Finset.sum Finset.univ fun x => v x * (det M * Pi.single i 1 x)
rw [Finset.sum_eq_single i, Pi.single_eq_same, mul_one]
case h.e'_2.h₀
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
j : m
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ v j * (det M * Pi.single i 1 j) = 0
case h.e'_2.h₀
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ i → v b * (det M * Pi.single i 1 b) = 0
intro j _ hj
no goals
case h.e'_2.h₀
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
j : m
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ v j * (det M * Pi.single i 1 j) = 0
simp [hj]
case h.e'_2.h₁
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
a✝ : ¬i ∈ Finset.univ
⊢ v i * (det M * Pi.single i 1 i) = 0
case h.e'_2.h₁
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ ¬i ∈ Finset.univ → v i * (det M * Pi.single i 1 i) = 0
intros
case h.e'_2.h₁
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
a✝ : ¬i ∈ Finset.univ
this : i ∈ Finset.univ
⊢ v i * (det M * Pi.single i 1 i) = 0
case h.e'_2.h₁
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
a✝ : ¬i ∈ Finset.univ
⊢ v i * (det M * Pi.single i 1 i) = 0
have := Finset.mem_univ i
no goals
case h.e'_2.h₁
m : Type u_1
R : Type ?u.4064
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
a✝ : ¬i ∈ Finset.univ
this : i ∈ Finset.univ
⊢ v i * (det M * Pi.single i 1 i) = 0
contradiction