Skip to content

refactor: Separate Vector.Basic & CoVector.Basic#1050

Open
jstoobysmith wants to merge 3 commits intomasterfrom
VectorTensorial
Open

refactor: Separate Vector.Basic & CoVector.Basic#1050
jstoobysmith wants to merge 3 commits intomasterfrom
VectorTensorial

Conversation

@jstoobysmith
Copy link
Copy Markdown
Member

Separating the modules Vector.Basic and CoVector.Basic into parts which depend on the Tensorial instance, and parts which are independent of the Tensorial instance.

This will help with #1048

Comment thread Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean Outdated
@jstoobysmith jstoobysmith added RFC Request for comment t-relativity Relativity labels Apr 21, 2026
@jstoobysmith
Copy link
Copy Markdown
Member Author

(Sorry @morrison-daniel asked you to review this before noticing the merge conflict - so feel free to ignore.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

RFC Request for comment t-relativity Relativity

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant