feat(linear_algebra/trace): trace of projection maps (#14165)
This is proved under the `field` assumption instead of the finite free module assumptions generally used to talk about the trace because we need the submodules `p` and `f.ker` to also be free and finite.
- [x] depends on: #13872
Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
