case mp
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤ → IsUnit (↑(Basis.det e) v)

case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ IsUnit (↑(Basis.det e) v) → LinearIndependent R v ∧ span R (Set.range v) = ⊤
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤ ↔ IsUnit (↑(Basis.det e) v)
constructor
case mp.intro
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
⊢ IsUnit (↑(Basis.det e) v)
case mp
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤ → IsUnit (↑(Basis.det e) v)
rintro ⟨hli, hspan⟩
case mp.intro
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli (_ : ⊤ ≤ span R (Set.range v))
⊢ IsUnit (↑(Basis.det e) v)
case mp.intro
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
⊢ IsUnit (↑(Basis.det e) v)
set v' := Basis.mk hli hspan.ge
case mp.intro
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli (_ : ⊤ ≤ span R (Set.range v))
⊢ IsUnit (det (Basis.toMatrix e v))
case mp.intro
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli (_ : ⊤ ≤ span R (Set.range v))
⊢ IsUnit (↑(Basis.det e) v)
rw [e.det_apply]
case h.e'_3.h.e'_6
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli (_ : ⊤ ≤ span R (Set.range v))
⊢ Basis.toMatrix e v = ↑(toMatrix v' e) ↑(LinearEquiv.refl R M)
case mp.intro
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli (_ : ⊤ ≤ span R (Set.range v))
⊢ IsUnit (det (Basis.toMatrix e v))
convert LinearEquiv.isUnit_det (LinearEquiv.refl R M) v' e using 2
case h.e'_3.h.e'_6.a.h
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli (_ : ⊤ ≤ span R (Set.range v))
i j : ι
⊢ Basis.toMatrix e v i j = ↑(toMatrix v' e) (↑(LinearEquiv.refl R M)) i j
case h.e'_3.h.e'_6
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli (_ : ⊤ ≤ span R (Set.range v))
⊢ Basis.toMatrix e v = ↑(toMatrix v' e) ↑(LinearEquiv.refl R M)
ext (i j)
no goals
case h.e'_3.h.e'_6.a.h
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli (_ : ⊤ ≤ span R (Set.range v))
i j : ι
⊢ Basis.toMatrix e v i j = ↑(toMatrix v' e) (↑(LinearEquiv.refl R M)) i j
simp
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (↑(Basis.det e) v)
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ IsUnit (↑(Basis.det e) v) → LinearIndependent R v ∧ span R (Set.range v) = ⊤
intro h
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (↑(Basis.det e) v)
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
rw [Basis.det_apply, Basis.toMatrix_eq_toMatrix_constr] at h
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
v' : Basis ι R M := Basis.map e (LinearEquiv.ofIsUnitDet h)
v'_def : v' = Basis.map e (LinearEquiv.ofIsUnitDet h)
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
set v' := Basis.map e (LinearEquiv.ofIsUnitDet h) with v'_def
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
v' : Basis ι R M := Basis.map e (LinearEquiv.ofIsUnitDet h)
v'_def : v' = Basis.map e (LinearEquiv.ofIsUnitDet h)
this : ↑v' = v
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
v' : Basis ι R M := Basis.map e (LinearEquiv.ofIsUnitDet h)
v'_def : v' = Basis.map e (LinearEquiv.ofIsUnitDet h)
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
have : ⇑v' = v := by
  ext i
  rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
v' : Basis ι R M := Basis.map e (LinearEquiv.ofIsUnitDet h)
v'_def : v' = Basis.map e (LinearEquiv.ofIsUnitDet h)
this : ↑v' = v
⊢ LinearIndependent R ↑v' ∧ span R (Set.range ↑v') = ⊤
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
v' : Basis ι R M := Basis.map e (LinearEquiv.ofIsUnitDet h)
v'_def : v' = Basis.map e (LinearEquiv.ofIsUnitDet h)
this : ↑v' = v
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤
rw [← this]
no goals
case mpr
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
v' : Basis ι R M := Basis.map e (LinearEquiv.ofIsUnitDet h)
v'_def : v' = Basis.map e (LinearEquiv.ofIsUnitDet h)
this : ↑v' = v
⊢ LinearIndependent R ↑v' ∧ span R (Set.range ↑v') = ⊤
exact ⟨v'.linearIndependent, v'.span_eq⟩
case h
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
v' : Basis ι R M := Basis.map e (LinearEquiv.ofIsUnitDet h)
v'_def : v' = Basis.map e (LinearEquiv.ofIsUnitDet h)
i : ι
⊢ ↑v' i = v i
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
v' : Basis ι R M := Basis.map e (LinearEquiv.ofIsUnitDet h)
v'_def : v' = Basis.map e (LinearEquiv.ofIsUnitDet h)
⊢ ↑v' = v
ext i
no goals
case h
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2551624
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit (det (↑(toMatrix e e) (↑(Basis.constr e ℕ) v)))
v' : Basis ι R M := Basis.map e (LinearEquiv.ofIsUnitDet h)
v'_def : v' = Basis.map e (LinearEquiv.ofIsUnitDet h)
i : ι
⊢ ↑v' i = v i
rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]