[Merged by Bors] - feat(data/matrix/basic): miscellaneous defs and lemmas by l534zhan · Pull Request #8289 · leanprover-community/mathlib3

l534zhan · 2021-07-13T11:01:09Z

miscellaneous defs and lemmas

depends on: [Merged by Bors] - feat(data/matrix/basic): add conj_transpose #8291
depends on: [Merged by Bors] - chore(data/matrix/basic): add lemmas about dot_product and mul_vec #8325

eric-wieser

IMO this PR changes far too many things at once, especially since you don't really describe the motivation for the changes.

Can you make a new PR that just adds conj_transpose and the things you need for it? We can then come back to this PR after that simpler one is merged.

l534zhan · 2021-07-13T11:12:04Z

IMO this PR changes far too many things at once, especially since you don't really describe the motivation for the changes.

Can you make a new PR that just adds conj_transpose and the things you need for it? We can then come back to this PR after that simpler one is merged.

Yes, sure.

src/data/matrix/basic.lean

As requested by Eric Wieser, I pulled one single change of #8289 out into a new PR. As such, this PR will not block anything in #8289. Co-authored-by: l534zhan <84618936+l534zhan@users.noreply.github.com>

src/data/matrix/basic.lean

l534zhan · 2021-07-13T21:42:11Z

@eric-wieser I will look at your suggestions in detail tomorrow. Could you let me know the first command I need to run for my local version, git pull or something else?

eric-wieser · 2021-07-13T21:46:20Z

git pull should work fine. I took the liberty of attempting to resolve the conflicts myself to make it easier for you, although I didn't do a perfect job of it - there are now two copies of transpose and conj_transpose, and you'll need to decide which one to keep.

bors · 2023-04-20T16:38:22Z

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

src/data/matrix/block.lean

YaelDillies · 2023-04-20T17:15:11Z

bors merge

miscellaneous defs and lemmas Co-authored-by: l534zhan <luming.zhang@merton.ox.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: l534zhan <84618936+l534zhan@users.noreply.github.com>

bors · 2023-04-20T20:01:03Z

Build failed (retrying...):

Lint mathlib

miscellaneous defs and lemmas Co-authored-by: l534zhan <luming.zhang@merton.ox.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: l534zhan <84618936+l534zhan@users.noreply.github.com>

bors · 2023-04-20T22:04:28Z

Build failed:

Lint mathlib

eric-wieser · 2023-04-21T08:02:27Z

Looks like there's an unrelated timeout

YaelDillies · 2023-04-21T11:36:29Z

bors merge

miscellaneous defs and lemmas Co-authored-by: l534zhan <luming.zhang@merton.ox.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: l534zhan <84618936+l534zhan@users.noreply.github.com>

Yael addressed my complains

bors · 2023-04-21T16:28:58Z

Pull request successfully merged into master.

Build succeeded:

Match leanprover-community/mathlib3#8289 * [`data.matrix.basic`@`0e2aab2b0d521f060f62a14d2cf2e2c54e8491d6`..`eba5bb3155cab51d80af00e8d7d69fa271b1302b`](https://leanprover-community.github.io/mathlib-port-status/file/data/matrix/basic?range=0e2aab2b0d521f060f62a14d2cf2e2c54e8491d6..eba5bb3155cab51d80af00e8d7d69fa271b1302b)

Match leanprover-community/mathlib3#8289 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Match leanprover-community/mathlib3#8289 [`data.matrix.block`@`3e068ece210655b7b9a9477c3aff38a492400aa1`..`eba5bb3155cab51d80af00e8d7d69fa271b1302b`](https://leanprover-community.github.io/mathlib-port-status/file/data/matrix/block?range=3e068ece210655b7b9a9477c3aff38a492400aa1..eba5bb3155cab51d80af00e8d7d69fa271b1302b)

Match leanprover-community/mathlib3#8289 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Match leanprover-community/mathlib3#8289 [`data.matrix.block`@`3e068ece210655b7b9a9477c3aff38a492400aa1`..`eba5bb3155cab51d80af00e8d7d69fa271b1302b`](https://leanprover-community.github.io/mathlib-port-status/file/data/matrix/block?range=3e068ece210655b7b9a9477c3aff38a492400aa1..eba5bb3155cab51d80af00e8d7d69fa271b1302b)

Match leanprover-community/mathlib3#8289 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Match leanprover-community/mathlib3#8289 [`data.matrix.block`@`3e068ece210655b7b9a9477c3aff38a492400aa1`..`eba5bb3155cab51d80af00e8d7d69fa271b1302b`](https://leanprover-community.github.io/mathlib-port-status/file/data/matrix/block?range=3e068ece210655b7b9a9477c3aff38a492400aa1..eba5bb3155cab51d80af00e8d7d69fa271b1302b)

Match leanprover-community/mathlib3#8289 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Match leanprover-community/mathlib3#8289 [`data.matrix.block`@`3e068ece210655b7b9a9477c3aff38a492400aa1`..`eba5bb3155cab51d80af00e8d7d69fa271b1302b`](https://leanprover-community.github.io/mathlib-port-status/file/data/matrix/block?range=3e068ece210655b7b9a9477c3aff38a492400aa1..eba5bb3155cab51d80af00e8d7d69fa271b1302b)

miscellaneous defs and lemmas

6c65a6e

l534zhan added the awaiting-review The author would like community review of the PR label Jul 13, 2021

l534zhan requested review from eric-wieser and jcommelin July 13, 2021 11:05

eric-wieser suggested changes Jul 13, 2021

View reviewed changes

eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 13, 2021

l534zhan mentioned this pull request Jul 13, 2021

[Merged by Bors] - feat(data/matrix/basic): add conj_transpose #8291

Closed

l534zhan added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 13, 2021

l534zhan requested a review from eric-wieser July 13, 2021 11:26

eric-wieser reviewed Jul 13, 2021

View reviewed changes

src/data/matrix/basic.lean Outdated Show resolved Hide resolved

Ruben-VandeVelde reviewed Jul 13, 2021

View reviewed changes

src/data/matrix/basic.lean Outdated Show resolved Hide resolved

fixed typos

3ca697c

eric-wieser reviewed Jul 13, 2021

View reviewed changes

src/data/matrix/basic.lean Outdated Show resolved Hide resolved

l534zhan added 2 commits July 13, 2021 13:40

fixed typos

5f58636

fixed things

7e7684a

l534zhan requested a review from Ruben-VandeVelde July 13, 2021 12:53

l534zhan mentioned this pull request Jul 13, 2021

[Merged by Bors] - chore(data/matrix/block): move block matrices into their own file #8290

Closed

l534zhan requested a review from eric-wieser July 13, 2021 12:57

github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 13, 2021

Merge branch 'master' into matrix_lz

75a4d4a

github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 13, 2021

eric-wieser reviewed Jul 13, 2021

View reviewed changes

src/data/matrix/basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jul 13, 2021

View reviewed changes

src/data/matrix/basic.lean Outdated Show resolved Hide resolved

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 20, 2023

eric-wieser reviewed Apr 20, 2023

View reviewed changes

src/data/matrix/block.lean Outdated Show resolved Hide resolved

use ⬝ᵥ notation

239f5ab

fix lint

ef549bd

bors bot changed the title ~~feat(data/matrix/basic): miscellaneous defs and lemmas~~ [Merged by Bors] - feat(data/matrix/basic): miscellaneous defs and lemmas Apr 21, 2023

bors bot closed this Apr 21, 2023

bors bot deleted the matrix_lz branch April 21, 2023 16:29

YaelDillies mentioned this pull request Apr 22, 2023

[Merged by Bors] - feat: Miscellaneous defs and lemmas leanprover-community/mathlib4#3589

Closed

bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 24, 2023

feat: Miscellaneous defs and lemmas (#3589)

67d9267

Match leanprover-community/mathlib3#8289 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

YaelDillies mentioned this pull request Apr 25, 2023

[Merged by Bors] - feat: Dot product of block matrices leanprover-community/mathlib4#3642

Closed

kim-em pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 10, 2023

feat: Miscellaneous defs and lemmas (#3589)

7a6b2bc

Match leanprover-community/mathlib3#8289 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

hrmacbeth pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 10, 2023

feat: Miscellaneous defs and lemmas (#3589)

e3bd98b

Match leanprover-community/mathlib3#8289 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

hrmacbeth pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 11, 2023

feat: Miscellaneous defs and lemmas (#3589)

67f7270

Match leanprover-community/mathlib3#8289 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Conversation

l534zhan commented Jul 13, 2021 • edited by eric-wieser Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

eric-wieser left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

l534zhan commented Jul 13, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

l534zhan commented Jul 13, 2021

Uh oh!

eric-wieser commented Jul 13, 2021

Uh oh!

bors bot commented Apr 20, 2023

Uh oh!

Uh oh!

YaelDillies commented Apr 20, 2023

Uh oh!

bors bot commented Apr 20, 2023

Uh oh!

bors bot commented Apr 20, 2023

Uh oh!

eric-wieser commented Apr 21, 2023

Uh oh!

YaelDillies commented Apr 21, 2023

Uh oh!

bors bot commented Apr 21, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

l534zhan commented Jul 13, 2021 •

edited by eric-wieser

Loading

eric-wieser left a comment •

edited

Loading