Skip to content

[Merged by Bors] - fix: denote alternating map by ⋀, not Λ#11064

Closed
bustercopley wants to merge 4 commits intomasterfrom
bigwedge
Closed

[Merged by Bors] - fix: denote alternating map by ⋀, not Λ#11064
bustercopley wants to merge 4 commits intomasterfrom
bigwedge

Conversation

@bustercopley
Copy link
Copy Markdown
Contributor

That is, \bigwedge, not \Lambda


Open in Gitpod

@bustercopley bustercopley changed the title fix: denote exterior power and alternating map by ⋀, not Λ fix: denote alternating map by ⋀, not Λ Feb 29, 2024
@bustercopley
Copy link
Copy Markdown
Contributor Author

Zulip

bustercopley added a commit that referenced this pull request Feb 29, 2024
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Mar 1, 2024
@bustercopley bustercopley removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 1, 2024
@bustercopley
Copy link
Copy Markdown
Contributor Author

force-push: timestamps only. (The commit took several minutes to update the PR. This was just for troubleshooting, and was unnecessary, as it turns out.)

Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors merge

Thanks!

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Mar 1, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 1, 2024
That is, `\bigwedge`, not `\Lambda`




Co-authored-by: Richard Copley <rcopley@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 1, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Mar 1, 2024
That is, `\bigwedge`, not `\Lambda`




Co-authored-by: Richard Copley <rcopley@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix: denote alternating map by ⋀, not Λ [Merged by Bors] - fix: denote alternating map by ⋀, not Λ Mar 1, 2024
@mathlib-bors mathlib-bors bot closed this Mar 1, 2024
@mathlib-bors mathlib-bors bot deleted the bigwedge branch March 1, 2024 18:37
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
That is, `\bigwedge`, not `\Lambda`




Co-authored-by: Richard Copley <rcopley@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
That is, `\bigwedge`, not `\Lambda`




Co-authored-by: Richard Copley <rcopley@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
utensil pushed a commit that referenced this pull request Mar 26, 2024
That is, `\bigwedge`, not `\Lambda`




Co-authored-by: Richard Copley <rcopley@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
That is, `\bigwedge`, not `\Lambda`




Co-authored-by: Richard Copley <rcopley@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants