Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
wants to merge 4 commits into from

Conversation

bustercopley
Copy link
Collaborator

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
Collaborator 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
Collaborator 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
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!

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot 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 <[email protected]>
Co-authored-by: Patrick Massot <[email protected]>
@mathlib-bors
Copy link
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 <[email protected]>
Co-authored-by: Patrick Massot <[email protected]>
@mathlib-bors
Copy link
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 <[email protected]>
Co-authored-by: Patrick Massot <[email protected]>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
That is, `\bigwedge`, not `\Lambda`




Co-authored-by: Richard Copley <[email protected]>
Co-authored-by: Patrick Massot <[email protected]>
utensil pushed a commit that referenced this pull request Mar 26, 2024
That is, `\bigwedge`, not `\Lambda`




Co-authored-by: Richard Copley <[email protected]>
Co-authored-by: Patrick Massot <[email protected]>
Louddy pushed a commit that referenced this pull request Apr 15, 2024
That is, `\bigwedge`, not `\Lambda`




Co-authored-by: Richard Copley <[email protected]>
Co-authored-by: Patrick Massot <[email protected]>
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.

5 participants