R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i : ι
⊢ ∀ (i_1 : ι),
    ↑(↑(det e) v • coord (Basis.mk hli hsp) i) (↑(Basis.mk hli hsp) i_1) =
      ↑(MultilinearMap.toLinearMap (↑(det e)) v i) (↑(Basis.mk hli hsp) i_1)
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i : ι
⊢ ↑(det e) v • coord (Basis.mk hli hsp) i = MultilinearMap.toLinearMap (↑(det e)) v i
apply (Basis.mk hli hsp).ext
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
⊢ ↑(↑(det e) v • coord (Basis.mk hli hsp) i) (↑(Basis.mk hli hsp) k) =
    ↑(MultilinearMap.toLinearMap (↑(det e)) v i) (↑(Basis.mk hli hsp) k)
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i : ι
⊢ ∀ (i_1 : ι),
    ↑(↑(det e) v • coord (Basis.mk hli hsp) i) (↑(Basis.mk hli hsp) i_1) =
      ↑(MultilinearMap.toLinearMap (↑(det e)) v i) (↑(Basis.mk hli hsp) i_1)
intro k
case inl
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ ↑(det e) v * ↑(coord (Basis.mk hli hsp) k) (v k) = ↑↑(det e) (update v k (v k))

case inr
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
hik : k ≠ i
⊢ ↑(det e) v * ↑(coord (Basis.mk hli hsp) i) (v k) = ↑↑(det e) (update v i (v k))
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
⊢ ↑(↑(det e) v • coord (Basis.mk hli hsp) i) (↑(Basis.mk hli hsp) k) =
    ↑(MultilinearMap.toLinearMap (↑(det e)) v i) (↑(Basis.mk hli hsp) k)
rcases eq_or_ne k i with (rfl | hik) <;>
  simp only [Algebra.id.smul_eq_mul, Basis.coe_mk, LinearMap.smul_apply, LinearMap.coe_mk,
    MultilinearMap.toLinearMap_apply]
case inl
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ ↑(det e) v = ↑↑(det e) v
case inl
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ ↑(det e) v * ↑(coord (Basis.mk hli hsp) k) (v k) = ↑↑(det e) (update v k (v k))
rw [Basis.mk_coord_apply_eq, mul_one, update_eq_self]
no goals
case inl
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
k : ι
⊢ ↑(det e) v = ↑↑(det e) v
congr
case inr
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
hik : k ≠ i
⊢ ↑↑(det e) (update v i (v k)) = 0
case inr
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
hik : k ≠ i
⊢ ↑(det e) v * ↑(coord (Basis.mk hli hsp) i) (v k) = ↑↑(det e) (update v i (v k))
rw [Basis.mk_coord_apply_ne hik, MulZeroClass.mul_zero, eq_comm]
no goals
case inr
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
hik : k ≠ i
⊢ ↑↑(det e) (update v i (v k)) = 0
exact e.det.map_eq_zero_of_eq _ (by simp [hik, Function.update_apply]) hik
no goals
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2746027
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2747047
inst✝¹ : CommRing A
inst✝ : Module A M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
i k : ι
hik : k ≠ i
⊢ update v i (v k) k = update v i (v k) i
simp [hik, Function.update_apply]