mathlib3
feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices.
#1913

Merged

feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices. #1913

mergify merged 10 commits into master from ocfnash/matrix_trace_commute

feat(linear_algebra/matrix): trace AB = trace BA

20fa11e6

Remove now-redundant matrix.smul_sum

928fde54

ChrisHughes24 commented on 2020-01-27

Make arguments explicit for matrix.trace, matrix.diag

ad1ef09f

Tidy up whitespace

20f07a7c

Remove now-redundant type ascriptions

75fcf765

jcommelin commented on 2020-01-28

ocfnash changed the title ~~ocfnash/matrix trace commute~~ Add proof that trace AB = trace BA, for matrices. 6 years ago

Update src/linear_algebra/matrix.lean

2c431003

Feedback from code review

2a209d9d

Generalize diag_transpose, trace_transpose.

d68eb9d5

jcommelin changed the title ~~Add proof that trace AB = trace BA, for matrices.~~ feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices. 6 years ago

robertylewis added awaiting-review

ChrisHughes24 commented on 2020-01-30

Explicit arguments trace, diag defs but not lemmas

da1d5aca

ChrisHughes24 added ready-to-merge

ChrisHughes24 removed awaiting-review

ChrisHughes24 approved these changes on 2020-01-31

Merge branch 'master' into ocfnash/matrix_trace_commute

3bd5b423

mergify merged 5ce0c0a2 into master 6 years ago

mergify deleted the ocfnash/matrix_trace_commute branch 6 years ago

Reviewers

ChrisHughes24

digama0

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices. #1913 Merged

feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices. #1913

mathlib3
feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices.
#1913

Merged