R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2243677
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type ?u.2244219
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ ∀ (x : M), ↑(comp f ↑e) x = ↑(comp f ↑e') (↑(LinearEquiv.trans e (LinearEquiv.symm e')) x)
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2243677
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type ?u.2244219
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ Associated (↑LinearMap.det (comp f ↑e)) (↑LinearMap.det (comp f ↑e'))
refine' LinearMap.associated_det_of_eq_comp (e.trans e'.symm) _ _ _
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2243677
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type ?u.2244219
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
x : M
⊢ ↑(comp f ↑e) x = ↑(comp f ↑e') (↑(LinearEquiv.trans e (LinearEquiv.symm e')) x)
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2243677
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type ?u.2244219
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ ∀ (x : M), ↑(comp f ↑e) x = ↑(comp f ↑e') (↑(LinearEquiv.trans e (LinearEquiv.symm e')) x)
intro x
no goals
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2243677
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type ?u.2244219
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
x : M
⊢ ↑(comp f ↑e) x = ↑(comp f ↑e') (↑(LinearEquiv.trans e (LinearEquiv.symm e')) x)
simp only [LinearMap.comp_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
  LinearEquiv.apply_symm_apply]