R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M ↔ ¬∃ v x, vecMul v M = 0
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M ↔ det M ≠ 0
refine' Iff.trans _ (not_iff_not.mpr exists_vecMul_eq_zero_iff)
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M ↔ ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M ↔ ¬∃ v x, vecMul v M = 0
simp only [not_exists]
case mp
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M → ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0

case mpr
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ (∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0) → Nondegenerate M
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M ↔ ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
constructor
case mp
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : Nondegenerate M
v : n → A
hv : v ≠ 0
hMv : vecMul v M = 0
⊢ False
case mp
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M → ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
intro hM v hv hMv
case mp.intro
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : Nondegenerate M
v : n → A
hv : v ≠ 0
hMv : vecMul v M = 0
w : n → A
hwMv : v ⬝ᵥ mulVec M w ≠ 0
⊢ False
case mp
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : Nondegenerate M
v : n → A
hv : v ≠ 0
hMv : vecMul v M = 0
⊢ False
obtain ⟨w, hwMv⟩ := hM.exists_not_ortho_of_ne_zero hv
no goals
case mp.intro
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : Nondegenerate M
v : n → A
hv : v ≠ 0
hMv : vecMul v M = 0
w : n → A
hwMv : v ⬝ᵥ mulVec M w ≠ 0
⊢ False
simp [dotProduct_mulVec, hMv, zero_dotProduct, ne_eq, not_true] at hwMv
case mpr
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ mulVec M w = 0
⊢ v = 0
case mpr
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ (∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0) → Nondegenerate M
intro h v hv
case mpr
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ mulVec M w = 0
i : n
⊢ vecMul v M i = OfNat.ofNat 0 i
case mpr
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ mulVec M w = 0
⊢ v = 0
refine' not_imp_not.mp (h v) (funext fun i => _)
no goals
case mpr
R : Type ?u.534603
M✝ : Type ?u.534606
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M✝
inst✝⁴ : Module R M✝
n : Type u_2
inst✝³ : Fintype n
A : Type u_1
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ mulVec M w = 0
i : n
⊢ vecMul v M i = OfNat.ofNat 0 i
simpa only [dotProduct_mulVec, dotProduct_single, mul_one] using hv (Pi.single i 1)