[Merged by Bors] - feat(linear_algebra/matrix): trace of an endomorphism independent of basis

[kckennylau]

---

[ocfnash]

I'm delighted to see someone finally defining traces; nice work!

Ages ago I had plans to do this and was planning to define the trace by showing that dual_tensor_hom was a bijection when we needed it to be (e.g., when there exists bases) and then composing its inverse with contract_left. If it was easy, it might be nice if we had some lemmas connecting the definition here with this approach.

[jcommelin]

Shouldn't this be in a different namespace? linear_map.trace?

[jcommelin]

@kckennylau What do you think of @ocfnash 's suggestion? That way the definition is intrinsically independent of a basis. And given a basis, you turn the linear map into a matrix, and relate the linear_map.trace to matrix.trace.

[kckennylau]

@jcommelin could we relate those in another PR?

[jcommelin]

@kckennylau We could do that, but I guess it means that the next PR would refactor the definition and lemmas about linear_map.trace. Something like trace_apply is not the statement that would be natural with the other definition.

[kckennylau]

the next PR can just be (linear_map.trace R M).comp (dual_tensor_hom R M M) = contract_left R M

[jcommelin]

@kckennylau You don't like "Linear algebra done right"?
Anyway, I don't really care about what the definition is, if all the lemmas are there.

[jcommelin]

Thanks 🎉

bors merge

looking forward to the next PR

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs