Skip to content

[Merged by Bors] - feat: FiberBundle.extend#36234

Closed
PatrickMassot wants to merge 5 commits intoleanprover-community:masterfrom
PatrickMassot:pm_extend
Closed

[Merged by Bors] - feat: FiberBundle.extend#36234
PatrickMassot wants to merge 5 commits intoleanprover-community:masterfrom
PatrickMassot:pm_extend

Conversation

@PatrickMassot
Copy link
Copy Markdown
Member

@PatrickMassot PatrickMassot commented Mar 5, 2026 •
edited by grunweg
Loading

Extend an element of a fiber at a point to a local section.

From the path towards Riemannian geometry.

Co-authored-by: Michael Rothgang rothgang@math.uni-bonn.de
Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com

Open in Gitpod

@PatrickMassot
feat: FiberBundle.extend
4dc88fe 
Extend an element of a fiber at a point to a local section.
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 5, 2026 •
edited
Loading

PR summary 760db6fd3b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ contMDiffAt_extend'
+ exists_contMDiffOn_extend
+ exists_mdifferentiableOn_extend
+ extend
+ extend_apply_self
+ mdifferentiableAt_extend

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg
grunweg reviewed Mar 6, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

A few more cosmetic comments - otherwise, LGTM (and we should discuss procedures for merging)

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Mar 6, 2026

Also, should we all three be co-authors of this one? Or at least Heather? (minor question; I'm happy to edit the PR description myself if we think so)

@grunweg grunweg added awaiting-author A reviewer has asked the author a question or requested changes. t-differential-geometry Manifolds etc labels Mar 6, 2026
@PatrickMassot PatrickMassot mentioned this pull request Mar 6, 2026
Closed
1 task
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Mar 6, 2026

Looks good to me, let's get this in! (For the record: Heather rewrote this definition, Patrick PRed it and I just reviewed it by golfing. Three maintainers together should do.)
bors merge

@mathlib-triage mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Mar 6, 2026
mathlib-bors bot pushed a commit that referenced this pull request Mar 6, 2026
@PatrickMassot @grunweg @hrmacbeth
feat: FiberBundle.extend (#36234)
cd3f041 
Extend an element of a fiber at a point to a local section.

From the path towards Riemannian geometry.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 6, 2026

This PR was included in a batch that was canceled, it will be automatically retried

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Mar 6, 2026

bors r+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 6, 2026

Already running a review

mathlib-bors bot pushed a commit that referenced this pull request Mar 6, 2026
@PatrickMassot @grunweg @hrmacbeth
feat: FiberBundle.extend (#36234)
f25d7a2 
Extend an element of a fiber at a point to a local section.

From the path towards Riemannian geometry.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Mar 6, 2026

bors r+

1 similar comment
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Mar 6, 2026

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 6, 2026
@PatrickMassot @grunweg @hrmacbeth
feat: FiberBundle.extend (#36234)
dce8fc3 
Extend an element of a fiber at a point to a local section.

From the path towards Riemannian geometry.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 6, 2026

This PR was included in a batch that was canceled, it will be automatically retried

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Mar 6, 2026

bors r+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 6, 2026

Already running a review

@hrmacbeth hrmacbeth mentioned this pull request Mar 6, 2026
Closed
1 task
mathlib-bors bot pushed a commit that referenced this pull request Mar 6, 2026
@PatrickMassot @grunweg @hrmacbeth
feat: FiberBundle.extend (#36234)
0bcc938 
Extend an element of a fiber at a point to a local section.

From the path towards Riemannian geometry.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
@hrmacbeth hrmacbeth mentioned this pull request Mar 6, 2026
Closed
2 tasks
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 6, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: FiberBundle.extend [Merged by Bors] - feat: FiberBundle.extend Mar 6, 2026
@mathlib-bors mathlib-bors bot closed this Mar 6, 2026
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 8, 2026
@PatrickMassot @grunweg
@hrmacbeth @xroblot
feat: FiberBundle.extend (leanprover-community#36234)
100b2e7 
Extend an element of a fiber at a point to a local section.

From the path towards Riemannian geometry.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 9, 2026
@PatrickMassot @grunweg
@hrmacbeth @xroblot
feat: FiberBundle.extend (leanprover-community#36234)
b85a70d 
Extend an element of a fiber at a point to a local section.

From the path towards Riemannian geometry.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
seewoo5 pushed a commit to seewoo5/mathlib4 that referenced this pull request Mar 9, 2026
@PatrickMassot @grunweg
@hrmacbeth @seewoo5
feat: FiberBundle.extend (leanprover-community#36234)
68374f7 
Extend an element of a fiber at a point to a local section.

From the path towards Riemannian geometry.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026
@PatrickMassot @grunweg
@hrmacbeth @xroblot
feat: FiberBundle.extend (leanprover-community#36234)
5109868 
Extend an element of a fiber at a point to a local section.

From the path towards Riemannian geometry.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@PatrickMassot @grunweg @bryangingechen @sgouezel