Trace of identity

Stream: Is there code for X?

[Antoine Labelle]

Is there somewhere a lemma saying that the trace of the identity map on a finite-dimensional vector space is the dimension of the space? I found the analogous lemma for matrices but not for linear maps.

[Antoine Labelle]

Oh and same question for trace being invariant under conjugation

[Eric Wieser]

Isn't the linear_map trace defined via a matrix anyway? If so, you can probably get the results you want by unfolding down to that matrix, if you don't want to wait for a better response here.

[Kyle Miller]

docs#matrix.trace_mul_cycle along with matrix inverse cancellation would give you invariance under conjugation, but that's still for matrices and not linear endomorphisms

[Antoine Labelle]

Yeah I guess that would work but I feel like we should have the linear map versions of these lemmas so that we can avoid working with bases if not needed

[Riccardo Brasca]

We have the characteristic polynomial of an endomorphism

[Riccardo Brasca]

Writing an API for the coefficients is in my todo list, but I got absorbed by flt-regular

[Kevin Buzzard]

The moment you say "n-dimensional" you have already picked a basis, done something with it, and checked it's independent of basis. You can't get away from picking a basis

[Kevin Buzzard]

But I agree the notions should be there for linear maps :-)