Skip to content

refactor: Split Vector and CoVector#1165

Open
jstoobysmith wants to merge 2 commits into
leanprover-community:masterfrom
jstoobysmith:Split-Vector
Open

refactor: Split Vector and CoVector#1165
jstoobysmith wants to merge 2 commits into
leanprover-community:masterfrom
jstoobysmith:Split-Vector

Conversation

@jstoobysmith

Copy link
Copy Markdown
Member

This is an updated version of #1050.

There are no new results.

This PR splits Vector.Basic into Vector.Basic (for the basic module structure) and Vector.Tensorial (for the tensorial nature). It does the same with CoVector.Basic.

Other files have had their imports modified to account for this change.

@jstoobysmith jstoobysmith added the t-relativity Relativity label Jun 10, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. 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 want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

@jstoobysmith jstoobysmith added the RFC Request for comment label Jun 10, 2026
@jstoobysmith

Copy link
Copy Markdown
Member Author

This is also part of #1048

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