Skip to content

feat(PhyslibAlpha): add line surface#1190

Merged
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
Robby955:line-surface
Jun 17, 2026
Merged

feat(PhyslibAlpha): add line surface#1190
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
Robby955:line-surface

Conversation

@Robby955

Copy link
Copy Markdown
Contributor

Summary

  • add the coordinate line surface API in PhyslibAlpha.SpaceAndTime.Space.Surfaces.Line
  • define the pushed-forward line measure, its temperate-growth instance, and the associated distribution
  • prove the embedded line has ambient volume zero

@github-actions

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.

@jstoobysmith jstoobysmith added the PhyslibAlpha Pull requests which are for modifications to PhyslibAlpha. label Jun 17, 2026
@jstoobysmith

Copy link
Copy Markdown
Member

Great! Looks good to me! Approved, and will merge shortly.

@jstoobysmith

Copy link
Copy Markdown
Member

Many thanks for your first PR :)

jstoobysmith
jstoobysmith approved these changes Jun 17, 2026
@jstoobysmith jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label Jun 17, 2026
@jstoobysmith jstoobysmith merged commit c23ad71 into leanprover-community:master Jun 17, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

PhyslibAlpha Pull requests which are for modifications to PhyslibAlpha. ready-to-merge This PR is approved and will be merged shortly

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants