R : Type ?u.2655796
inst✝⁹ : CommRing R
M : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type u_2
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ Matrix.det (toMatrix b' (↑f ∘ ↑b)) = Matrix.det (↑(LinearMap.toMatrix b b') f)
R : Type ?u.2655796
inst✝⁹ : CommRing R
M : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type u_2
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ ↑(det b') (↑f ∘ ↑b) = ↑LinearMap.det (LinearMap.comp f ↑(Basis.equiv b' b (Equiv.refl ι)))
rw [Basis.det_apply, ← LinearMap.det_toMatrix b', LinearMap.toMatrix_comp _ b, Matrix.det_mul,
  LinearMap.toMatrix_basis_equiv, Matrix.det_one, mul_one]
case e_M
R : Type ?u.2655796
inst✝⁹ : CommRing R
M : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type u_2
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ toMatrix b' (↑f ∘ ↑b) = ↑(LinearMap.toMatrix b b') f
R : Type ?u.2655796
inst✝⁹ : CommRing R
M : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type u_2
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ Matrix.det (toMatrix b' (↑f ∘ ↑b)) = Matrix.det (↑(LinearMap.toMatrix b b') f)
congr 1
case e_M.a.h
R : Type ?u.2655796
inst✝⁹ : CommRing R
M : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type u_2
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
i j : ι
⊢ toMatrix b' (↑f ∘ ↑b) i j = ↑(LinearMap.toMatrix b b') f i j
case e_M
R : Type ?u.2655796
inst✝⁹ : CommRing R
M : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type u_2
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ toMatrix b' (↑f ∘ ↑b) = ↑(LinearMap.toMatrix b b') f
ext (i j)
no goals
case e_M.a.h
R : Type ?u.2655796
inst✝⁹ : CommRing R
M : Type u_4
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type u_2
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
i j : ι
⊢ toMatrix b' (↑f ∘ ↑b) i j = ↑(LinearMap.toMatrix b b') f i j
rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply]