R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this :
  (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det (↑(RingHom.mapMatrix (algebraMap A K)) M) = 0
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
have : (∃ (v : _)(_ : v ≠ 0), mulVec ((algebraMap A K).mapMatrix M) v = 0) ↔ _ :=
  exists_mulVec_eq_zero_iff_aux
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this :
  (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det (↑(RingHom.mapMatrix (algebraMap A K)) M) = 0
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
rw [← RingHom.map_det, IsFractionRing.to_map_eq_zero_iff] at this
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
⊢ (∃ v x, mulVec M v = 0) ↔ ∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
refine' Iff.trans _ this
case mp.intro.intro
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
⊢ ∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0

case mpr.intro.intro
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
⊢ ∃ v x, mulVec M v = 0
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
⊢ (∃ v x, mulVec M v = 0) ↔ ∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
constructor <;> rintro ⟨v, hv, mul_eq⟩
case mp.intro.intro.refine'_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
h : (fun i => ↑(algebraMap A K) (v i)) = 0
i : n
⊢ v i = OfNat.ofNat 0 i

case mp.intro.intro.refine'_2
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
⊢ (mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) fun i => ↑(algebraMap A K) (v i)) = 0
case mp.intro.intro
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
⊢ ∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
refine' ⟨fun i => algebraMap _ _ (v i), mt (fun h => funext fun i => _) hv, _⟩
no goals
case mp.intro.intro.refine'_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
h : (fun i => ↑(algebraMap A K) (v i)) = 0
i : n
⊢ v i = OfNat.ofNat 0 i
exact IsFractionRing.to_map_eq_zero_iff.mp (congr_fun h i)
case mp.intro.intro.refine'_2.h
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
i : n
⊢ mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) (fun i => ↑(algebraMap A K) (v i)) i = OfNat.ofNat 0 i
case mp.intro.intro.refine'_2
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
⊢ (mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) fun i => ↑(algebraMap A K) (v i)) = 0
ext i
case mp.intro.intro.refine'_2.h
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
i : n
⊢ ↑(algebraMap A K) (mulVec (fun i j => M i j) (fun i => v i) i) = OfNat.ofNat 0 i
case mp.intro.intro.refine'_2.h
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
i : n
⊢ mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) (fun i => ↑(algebraMap A K) (v i)) i = OfNat.ofNat 0 i
refine' (RingHom.map_mulVec _ _ _ i).symm.trans _
no goals
case mp.intro.intro.refine'_2.h
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
i : n
⊢ ↑(algebraMap A K) (mulVec (fun i j => M i j) (fun i => v i) i) = OfNat.ofNat 0 i
rw [mul_eq, Pi.zero_apply, RingHom.map_zero, Pi.zero_apply]
case mpr.intro.intro
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
⊢ ∃ v x, mulVec M v = 0
case mpr.intro.intro
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
⊢ ∃ v x, mulVec M v = 0
letI := Classical.decEq K
case mpr.intro.intro.intro.mk
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
ba_eq : ∀ (a : K), a ∈ Finset.image v Finset.univ → IsLocalization.IsInteger A (↑{ val := b, property := hb } • a)
⊢ ∃ v x, mulVec M v = 0
case mpr.intro.intro
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
⊢ ∃ v x, mulVec M v = 0
obtain ⟨⟨b, hb⟩, ba_eq⟩ :=
  IsLocalization.exist_integer_multiples_of_finset (nonZeroDivisors A) (Finset.univ.image v)
case mpr.intro.intro.intro.mk
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
⊢ ∃ v x, mulVec M v = 0
case mpr.intro.intro.intro.mk
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
ba_eq : ∀ (a : K), a ∈ Finset.image v Finset.univ → IsLocalization.IsInteger A (↑{ val := b, property := hb } • a)
⊢ ∃ v x, mulVec M v = 0
choose f hf using ba_eq
case mpr.intro.intro.intro.mk.refine'_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
h : (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
i : n
⊢ v i = OfNat.ofNat 0 i

case mpr.intro.intro.intro.mk.refine'_2
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
⊢ (mulVec M fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
case mpr.intro.intro.intro.mk
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
⊢ ∃ v x, mulVec M v = 0
refine'
  ⟨fun i => f _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩),
    mt (fun h => funext fun i => _) hv, _⟩
case mpr.intro.intro.intro.mk.refine'_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝¹ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this✝ : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
h : (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
i : n
this : ↑(algebraMap A K) (f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = ↑(algebraMap A K) (OfNat.ofNat 0 i)
⊢ v i = OfNat.ofNat 0 i
case mpr.intro.intro.intro.mk.refine'_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
h : (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
i : n
⊢ v i = OfNat.ofNat 0 i
have := congr_arg (algebraMap A K) (congr_fun h i)
case mpr.intro.intro.intro.mk.refine'_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝¹ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this✝ : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
h : (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
i : n
this : b = 0 ∨ v i = 0
⊢ v i = OfNat.ofNat 0 i
case mpr.intro.intro.intro.mk.refine'_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝¹ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this✝ : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
h : (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
i : n
this : ↑(algebraMap A K) (f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = ↑(algebraMap A K) (OfNat.ofNat 0 i)
⊢ v i = OfNat.ofNat 0 i
rw [hf, Subtype.coe_mk, Pi.zero_apply, RingHom.map_zero, Algebra.smul_def, mul_eq_zero,
  IsFractionRing.to_map_eq_zero_iff] at this
no goals
case mpr.intro.intro.intro.mk.refine'_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝¹ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this✝ : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
h : (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
i : n
this : b = 0 ∨ v i = 0
⊢ v i = OfNat.ofNat 0 i
exact this.resolve_left (nonZeroDivisors.ne_zero hb)
case mpr.intro.intro.intro.mk.refine'_2.h
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ mulVec M (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) i = OfNat.ofNat 0 i
case mpr.intro.intro.intro.mk.refine'_2
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
⊢ (mulVec M fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
ext i
case mpr.intro.intro.intro.mk.refine'_2.h
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ ↑(algebraMap A K) (mulVec M (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) i) =
    ↑(algebraMap A K) (OfNat.ofNat 0 i)
case mpr.intro.intro.intro.mk.refine'_2.h
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ mulVec M (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) i = OfNat.ofNat 0 i
refine' IsFractionRing.injective A K _
case mpr.intro.intro.intro.mk.refine'_2.h.calc_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ ↑(algebraMap A K) (mulVec M (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) i) =
    mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) (↑(algebraMap A K) b • v) i

case mpr.intro.intro.intro.mk.refine'_2.h.calc_2
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) (↑(algebraMap A K) b • v) i = 0
case mpr.intro.intro.intro.mk.refine'_2.h
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ ↑(algebraMap A K) (mulVec M (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) i) =
    ↑(algebraMap A K) (OfNat.ofNat 0 i)
calc
  algebraMap A K (M.mulVec (fun i : n => f (v i) _) i) =
      ((algebraMap A K).mapMatrix M).mulVec (algebraMap _ K b • v) i := ?_
  _ = 0 := ?_
  _ = algebraMap A K 0 := (RingHom.map_zero _).symm
no goals
case mpr.intro.intro.intro.mk.refine'_2.h.calc_1
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ ↑(algebraMap A K) (mulVec M (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) i) =
    mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) (↑(algebraMap A K) b • v) i
simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf, Subtype.coe_mk,
  RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]
no goals
case mpr.intro.intro.intro.mk.refine'_2.h.calc_2
R : Type ?u.259223
M✝ : Type ?u.259226
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
n : Type u_3
inst✝⁶ : Fintype n
A : Type u_1
K : Type u_2
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) (↑(algebraMap A K) b • v) i = 0
rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]