more theory about matrix traces

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory

http://homotopytypetheory.org/

Other

1.23k stars 185 forks source link

Closed Alizter closed 1 month ago

Alizter commented 1 month ago

We prove that:

The trace of a matrix sum is the sum of traces.
The trace preserves scalar multiplication (it is a linear map)
In a commutative ring, a cyclic permutation of a product of matrices has invariant trace.