docs(Relativity): correct the CoVector rep docstring to say covectors - #1497
Conversation
The docstring is identical to the one on Lorentz.Vector.rep in the sibling file, which acts on Vector d; this one acts on CoVector d. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-authored-by: Claude <claude@users.noreply.github.com>
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
77e041b to
1d1c5ba
Compare
jstoobysmith
left a comment
There was a problem hiding this comment.
Looks great - approved, many thanks
|
Thanks for these first pull requests! Hope they are the first of many 🎉 |
|
Absolutely, hope to contribute much more - thanks! |
Closes #1495.
The docstring on
Lorentz.CoVector.repsays the representation acts on Lorentz vectors. It acts onCoVector d. The same line sits aboveLorentz.Vector.repinPhyslib/Relativity/Tensors/RealTensor/Vector/Representation.lean, where it is correct, so this looks like a copy where the type changed and the docstring did not.Docstring only, no declarations added or removed