R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
⊢ Associated (↑LinearMap.det (comp f' ↑e)) (↑LinearMap.det f')
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
⊢ Associated (↑LinearMap.det f) (↑LinearMap.det f')
suffices Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f') by
  convert this using 2
  ext x
  exact h x
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
⊢ Associated (↑LinearMap.det f' * ↑LinearMap.det ↑e) (↑LinearMap.det f' * 1)
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
⊢ Associated (↑LinearMap.det (comp f' ↑e)) (↑LinearMap.det f')
rw [← mul_one (LinearMap.det f'), LinearMap.det_comp]
no goals
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
⊢ Associated (↑LinearMap.det f' * ↑LinearMap.det ↑e) (↑LinearMap.det f' * 1)
exact Associated.mul_left _ (associated_one_iff_isUnit.mpr e.isUnit_det')
case h.e'_3.h.e'_6
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
this : Associated (↑LinearMap.det (comp f' ↑e)) (↑LinearMap.det f')
⊢ f = comp f' ↑e
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
this : Associated (↑LinearMap.det (comp f' ↑e)) (↑LinearMap.det f')
⊢ Associated (↑LinearMap.det f) (↑LinearMap.det f')
convert this using 2
case h.e'_3.h.e'_6.h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
this : Associated (↑LinearMap.det (comp f' ↑e)) (↑LinearMap.det f')
x : M
⊢ ↑f x = ↑(comp f' ↑e) x
case h.e'_3.h.e'_6
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
this : Associated (↑LinearMap.det (comp f' ↑e)) (↑LinearMap.det f')
⊢ f = comp f' ↑e
ext x
no goals
case h.e'_3.h.e'_6.h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type ?u.2104049
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type ?u.2104591
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e✝ : Basis ι R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), ↑f x = ↑f' (↑e x)
this : Associated (↑LinearMap.det (comp f' ↑e)) (↑LinearMap.det f')
x : M
⊢ ↑f x = ↑(comp f' ↑e) x
exact h x