Skip to content

feat: Add equivariance to ConjTensorSpecies - #1358

Merged
jstoobysmith merged 3 commits into
leanprover-community:masterfrom
jstoobysmith:ComplexTensorSpecies
Jul 14, 2026
Merged

feat: Add equivariance to ConjTensorSpecies#1358
jstoobysmith merged 3 commits into
leanprover-community:masterfrom
jstoobysmith:ComplexTensorSpecies

Conversation

@jstoobysmith

Copy link
Copy Markdown
Member

Adding an equivariance condition to ConjTensorSpecies, this will allow it to be used for conjugates of Weyl fermions etc.

Adding an equivaraince condition to ConjTensorSpecies
@jstoobysmith

Copy link
Copy Markdown
Member Author

@pariandrea FYI, you might be interested in this.

@github-actions

github-actions Bot commented Jul 2, 2026

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

@nateabr nateabr left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Overall this was great to read, for a beginner(myself) the proofs of conjEquiv_equivariant and conjT_equivariant were particularly informative. I hope it gets merged soon.

Comment thread Physlib/Relativity/Tensors/Conjugation/Basic.lean Outdated
Co-authored-by: nateabr <135662056+nateabr@users.noreply.github.com>
@morrison-daniel morrison-daniel added the ready-to-merge This PR is approved and will be merged shortly label Jul 13, 2026
@jstoobysmith
jstoobysmith merged commit c525a22 into leanprover-community:master Jul 14, 2026
8 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR is approved and will be merged shortly reviewer-approved

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants