R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.726554
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] N
g : N →ₗ[R] M
h : ↑(↑(compr₂ (llcomp R M N M) (trace R M)) g) f = ↑(↑(compr₂ (flip (llcomp R N M N)) (trace R N)) g) f
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.726554
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
have h := ext_iff.1 (ext_iff.1 (trace_comp_comm R M N) g) f
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.726554
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] N
g : N →ₗ[R] M
h : ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.726554
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] N
g : N →ₗ[R] M
h : ↑(↑(compr₂ (llcomp R M N M) (trace R M)) g) f = ↑(↑(compr₂ (flip (llcomp R N M N)) (trace R N)) g) f
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
simp only [llcomp_apply', compr₂_apply, flip_apply] at h
no goals
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.726554
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] N
g : N →ₗ[R] M
h : ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
exact h