R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type ?u.257671
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type ?u.257671
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
let ⟨s, ⟨b⟩⟩ := H
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type ?u.257671
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ Matrix.trace (↑(toMatrix b b) f ⬝ ↑(toMatrix b b) g) = Matrix.trace (↑(toMatrix b b) g ⬝ ↑(toMatrix b b) f)
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type ?u.257671
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]
no goals
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type ?u.257671
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ Matrix.trace (↑(toMatrix b b) f ⬝ ↑(toMatrix b b) g) = Matrix.trace (↑(toMatrix b b) g ⬝ ↑(toMatrix b b) f)
apply Matrix.trace_mul_comm
no goals
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type ?u.257671
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]