R : Type ?u.374035
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.374626
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.375168
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.376144
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
s : Finset M
b : Basis { x // x ∈ s } A M
f : M →ₗ[A] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ ↑LinearMap.det f = det (↑(toMatrix b b) f)
R : Type ?u.374035
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.374626
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.375168
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.376144
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
s : Finset M
b : Basis { x // x ∈ s } A M
f : M →ₗ[A] M
⊢ ↑LinearMap.det f = det (↑(toMatrix b b) f)
have : ∃ s : Finset M, Nonempty (Basis s A M) := ⟨s, ⟨b⟩⟩
no goals
R : Type ?u.374035
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.374626
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.375168
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.376144
inst✝¹ : Fintype κ
inst✝ : DecidableEq M
s : Finset M
b : Basis { x // x ∈ s } A M
f : M →ₗ[A] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ ↑LinearMap.det f = det (↑(toMatrix b b) f)
rw [LinearMap.coe_det, dif_pos, detAux_def'' _ b] <;> assumption