[Merged by Bors] - feat(linear_algebra/{cross_product,vectors}): cross product #11181

madvorak · 2022-01-01T16:17:27Z

Defines the cross product for R^3 and gives localized notation for that and the dot product.

Was #10959

Co-authored-by: Kyle Miller kmill31415@gmail.com
Co-authored-by: Eric Wieser wieser.eric@gmail.com

kmill

Looks good to me 👍

src/linear_algebra/vectors.lean

src/linear_algebra/cross_product.lean

eric-wieser

Is it worth including a few statements about u ×₃ v ×₃ w, or do you intend to leave that to a future PR? If so, can you add a TODO section in the module docstring, which should probably contains

The Jacobi identity
Generalization to an arbitrary 3D inner product space - I know we decided on Zulip it wasn't worth doing this, but we should record that decision in the docstring somewhere.

docstring comment for triple_product_eq_det Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…refactoring (simplification of names

… identity

madvorak · 2022-01-03T12:38:39Z

The Jacobi identity

I have just implemented it. Please, check the name and the docstring.

Generalization to an arbitrary 3D inner product space - I know we decided on Zulip it wasn't worth doing this, but we should record that decision in the docstring somewhere.

How should I put it into the docstring?
I suppose it should be in the main docstring for the file but I don't know how to formulate it. And should a link to the Zulip discussion be included?

src/linear_algebra/cross_product.lean

src/linear_algebra/vectors.lean

src/linear_algebra/cross_product.lean

jcommelin

Thanks 🎉

bors merge

Defines the cross product for R^3 and gives localized notation for that and the dot product. Was #10959 Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>

bors · 2022-01-13T09:33:38Z

Build failed (retrying...):

Lint style

Defines the cross product for R^3 and gives localized notation for that and the dot product. Was #10959 Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>

madvorak · 2022-01-13T10:17:30Z

bors r-

Does 100 characters and a newline count as >100 lines?

bors · 2022-01-13T10:17:31Z

Canceled.

…r-community/mathlib into madvorak_cross_product

madvorak · 2022-01-13T10:21:05Z

lemme try whether it allows me to rerun it

bors merge

bors · 2022-01-13T10:21:06Z

🔒 Permission denied

Existing reviewers: click here to make madvorak a reviewer

jcommelin · 2022-01-13T10:23:13Z

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

bors · 2022-01-13T10:23:14Z

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

eric-wieser · 2022-01-13T10:48:15Z

The long line wasn't in this PR, it was in #10269. By cancelling, you've just made things slower, bors already worked this out for you!

… different PR, revert del

madvorak · 2022-01-13T10:59:12Z

bors r+

erdOne · 2022-01-13T11:04:39Z

Its me :(
sorry about that confusion.

madvorak · 2022-01-13T11:05:29Z

Its me :( sorry about that confusion.

No worries.

BTW did my previous comment resume the merging?

madvorak · 2022-01-13T12:13:17Z

bors merge

bors · 2022-01-13T12:13:18Z

Already running a review

Defines the cross product for R^3 and gives localized notation for that and the dot product. Was #10959 Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>

bors · 2022-01-13T14:07:48Z

Pull request successfully merged into master.

Build succeeded:

feat(linear_algebra/cross_product)

448ef4d

madvorak mentioned this pull request Jan 1, 2022

feat(linear_algebra/cross-product): Cross product added #10959

Closed

kmill approved these changes Jan 1, 2022

View reviewed changes

refactor(linear_algebra/vectors): unused argument

06d1895

kmill added the awaiting-review The author would like community review of the PR label Jan 2, 2022

kmill changed the title ~~feat(linear_algebra/cross_product)~~ feat(linear_algebra/{cross_product,vectors}): cross product Jan 2, 2022

eric-wieser reviewed Jan 2, 2022

View reviewed changes

src/linear_algebra/vectors.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 2, 2022

View reviewed changes

src/linear_algebra/cross_product.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 2, 2022

View reviewed changes

src/linear_algebra/cross_product.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 2, 2022

View reviewed changes

src/linear_algebra/cross_product.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 2, 2022

View reviewed changes

src/linear_algebra/cross_product.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 2, 2022

View reviewed changes

src/linear_algebra/cross_product.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 2, 2022

View reviewed changes

madvorak removed the awaiting-review The author would like community review of the PR label Jan 3, 2022

madvorak and others added 3 commits January 3, 2022 11:21

Update src/linear_algebra/cross_product.lean

ed2a8bf

docstring comment for triple_product_eq_det Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

feat(linear_algebra/cross_product): added the jacobi identity; small …

408677e

…refactoring (simplification of names

refactor(linear_algebra/cross_product): shortened proof of the Jacobi…

924004d

… identity

eric-wieser reviewed Jan 4, 2022

View reviewed changes

src/linear_algebra/cross_product.lean Outdated Show resolved Hide resolved

eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 4, 2022

eric-wieser reviewed Jan 4, 2022

View reviewed changes

src/linear_algebra/vectors.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 4, 2022

View reviewed changes

src/linear_algebra/vectors.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 4, 2022

View reviewed changes

src/linear_algebra/vectors.lean Outdated Show resolved Hide resolved

feat(linear_algebra/cross_product): cross product is a lie ring

85cd4ff

eric-wieser reviewed Jan 4, 2022

View reviewed changes

src/linear_algebra/cross_product.lean Outdated Show resolved Hide resolved

feat(linear_algebra/cross_product): improved comments about the lie ring

cffd9c7

madvorak added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 4, 2022

refactor(linear_algebra/vectors): redundant parentheses removed

d95f2bc

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 Jan 4, 2022

madvorak added 2 commits January 13, 2022 02:15

refactor(linear_algebra/cross_product): little changes

d2c3cee

docs(linear_algebra/cross_product): Jacobi identity was renamed

6e1d89d

madvorak requested a review from jcommelin January 13, 2022 01:24

jcommelin reviewed Jan 13, 2022

View reviewed changes

src/linear_algebra/cross_product.lean Outdated Show resolved Hide resolved

Update src/linear_algebra/cross_product.lean

f2eb08c

jcommelin approved these changes Jan 13, 2022

View reviewed changes

fix(linear_algebra/cross_product): line too long

dde823a

Merge branch 'madvorak_cross_product' of https://github.com/leanprove…

73bdd43

…r-community/mathlib into madvorak_cross_product

github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label Jan 13, 2022

refactor(linear_algebra/cross_product): the problematic line was in a…

6660261

… different PR, revert del

bors bot changed the title ~~feat(linear_algebra/{cross_product,vectors}): cross product~~ [Merged by Bors] - feat(linear_algebra/{cross_product,vectors}): cross product Jan 13, 2022

bors bot closed this Jan 13, 2022

bors bot deleted the madvorak_cross_product branch January 13, 2022 14:07

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(linear_algebra/{cross_product,vectors}): cross product #11181

[Merged by Bors] - feat(linear_algebra/{cross_product,vectors}): cross product #11181

madvorak commented Jan 1, 2022 •

edited by kmill

kmill left a comment

eric-wieser left a comment •

edited

madvorak commented Jan 3, 2022

jcommelin left a comment

bors bot commented Jan 13, 2022

madvorak commented Jan 13, 2022

bors bot commented Jan 13, 2022

madvorak commented Jan 13, 2022

bors bot commented Jan 13, 2022

jcommelin commented Jan 13, 2022

bors bot commented Jan 13, 2022

eric-wieser commented Jan 13, 2022

madvorak commented Jan 13, 2022

erdOne commented Jan 13, 2022

madvorak commented Jan 13, 2022 •

edited

madvorak commented Jan 13, 2022

bors bot commented Jan 13, 2022

bors bot commented Jan 13, 2022

[Merged by Bors] - feat(linear_algebra/{cross_product,vectors}): cross product #11181

[Merged by Bors] - feat(linear_algebra/{cross_product,vectors}): cross product #11181

Conversation

madvorak commented Jan 1, 2022 • edited by kmill

kmill left a comment

Choose a reason for hiding this comment

eric-wieser left a comment • edited

Choose a reason for hiding this comment

madvorak commented Jan 3, 2022

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Jan 13, 2022

madvorak commented Jan 13, 2022

bors bot commented Jan 13, 2022

madvorak commented Jan 13, 2022

bors bot commented Jan 13, 2022

jcommelin commented Jan 13, 2022

bors bot commented Jan 13, 2022

eric-wieser commented Jan 13, 2022

madvorak commented Jan 13, 2022

erdOne commented Jan 13, 2022

madvorak commented Jan 13, 2022 • edited

madvorak commented Jan 13, 2022

bors bot commented Jan 13, 2022

bors bot commented Jan 13, 2022

madvorak commented Jan 1, 2022 •

edited by kmill

eric-wieser left a comment •

edited

madvorak commented Jan 13, 2022 •

edited