mathlib3
feat(linear_algebra/matrix): define the trace of a square matrix
#1883

Merged

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

mergify merged 11 commits into leanprover-community:master from matrix_trace

feat(linear_algebra/matrix): define the trace of a square matrix

06762e22

Move ring carrier to correct universe

84a82a95

cipher1024 assigned

ChrisHughes24 6 years ago

jcommelin commented on 2020-01-16

sgouezel added awaiting-author

Add lemma trace_one, and define diag as linear map

04218dcd

Define diag and trace solely as linear functions

74142334

Diag and trace for module-valued matrices

01f9f960

Fix cyclic import

70ecedff

jcommelin commented on 2020-01-21

Rename matrix.mul_sum' --> matrix.smul_sum

bdcfe97b

jcommelin commented on 2020-01-21

Merge branch 'master' into matrix_trace

d28f24a3

ChrisHughes24 added ready-to-merge

ChrisHughes24 removed awaiting-author

ChrisHughes24 approved these changes on 2020-01-26

Merge branch 'master' into matrix_trace

db442996

Trigger CI

4b085764

Merge branch 'master' into matrix_trace

e461630a

mergify merged 497e692b into master 6 years ago

ocfnash deleted the matrix_trace branch 6 years ago

Reviewers

ChrisHughes24

jcommelin

Assignees

ChrisHughes24

Labels

ready-to-merge

Milestone

No milestone