mathlib

497e692b - feat(linear_algebra/matrix): define the trace of a square matrix (#1883)

feat(linear_algebra/matrix): define the trace of a square matrix (#1883) * feat(linear_algebra/matrix): define the trace of a square matrix * Move ring carrier to correct universe * Add lemma trace_one, and define diag as linear map * Define diag and trace solely as linear functions * Diag and trace for module-valued matrices * Fix cyclic import * Rename matrix.mul_sum' --> matrix.smul_sum Co-Authored-By: Johan Commelin <johan@commelin.net> * Trigger CI Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>