case mp
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∃ v x, mulVec M v = 0) → det M = 0

case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ det M = 0 → ∃ v x, mulVec M v = 0
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
constructor
case mp.intro.intro
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
hv : v ≠ 0
mul_eq : mulVec M v = 0
⊢ det M = 0
case mp
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∃ v x, mulVec M v = 0) → det M = 0
rintro ⟨v, hv, mul_eq⟩
case mp.intro.intro
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
mul_eq : mulVec M v = 0
hv : det M ≠ 0
⊢ v = 0
case mp.intro.intro
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
hv : v ≠ 0
mul_eq : mulVec M v = 0
⊢ det M = 0
contrapose! hv
no goals
case mp.intro.intro
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
mul_eq : mulVec M v = 0
hv : det M ≠ 0
⊢ v = 0
exact eq_zero_of_mulVec_eq_zero hv mul_eq
case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0) → det M ≠ 0
case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ det M = 0 → ∃ v x, mulVec M v = 0
contrapose!
case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
⊢ det M ≠ 0
case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0) → det M ≠ 0
intro h
case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
⊢ det M ≠ 0
case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
⊢ det M ≠ 0
have : Function.Injective (Matrix.toLin' M) := by
  simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h
case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this✝ : Function.Injective ↑(↑toLin' M)
this : M ⬝ ↑toMatrix' ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this✝)) = 1
⊢ det M ≠ 0
case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
⊢ det M ≠ 0
have :
  M ⬝
      LinearMap.toMatrix'
        ((LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).symm : (n → K) →ₗ[K] n → K) =
    1 := by
  refine' Matrix.toLin'.injective (LinearMap.ext fun v => _)
  rw [Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix', LinearMap.comp_apply]
  exact (LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).apply_symm_apply v
no goals
case mpr
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this✝ : Function.Injective ↑(↑toLin' M)
this : M ⬝ ↑toMatrix' ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this✝)) = 1
⊢ det M ≠ 0
exact Matrix.det_ne_zero_of_right_inverse this
no goals
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
⊢ Function.Injective ↑(↑toLin' M)
simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
v : n → K
⊢ ↑(↑toLin' (M ⬝ ↑toMatrix' ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this)))) v = ↑(↑toLin' 1) v
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
⊢ M ⬝ ↑toMatrix' ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this)) = 1
refine' Matrix.toLin'.injective (LinearMap.ext fun v => _)
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
v : n → K
⊢ ↑(↑toLin' M) (↑↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this)) v) = ↑LinearMap.id v
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
v : n → K
⊢ ↑(↑toLin' (M ⬝ ↑toMatrix' ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this)))) v = ↑(↑toLin' 1) v
rw [Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix', LinearMap.comp_apply]
no goals
R : Type ?u.157867
M✝ : Type ?u.157870
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
n : Type u_2
inst✝² : Fintype n
K : Type u_1
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
v : n → K
⊢ ↑(↑toLin' M) (↑↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this)) v) = ↑LinearMap.id v
exact (LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).apply_symm_apply v