Skip to content

[Merged by Bors] - feat: contMDiffWithinAt_zeroSection#26676

Closed
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:Ckzerosection
Closed

[Merged by Bors] - feat: contMDiffWithinAt_zeroSection#26676
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:Ckzerosection

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jul 3, 2025

Part of the path towards geodesics and the Levi-Civita connection

Open in Gitpod

@grunweg
feat: contMDiffWithinAt_zeroSection
4fbef3f 
Part of the path towards geodesics and the Levi-Civita connection
@grunweg grunweg added the easy < 20s of review time. See the lifecycle page for guidelines. label Jul 3, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 3, 2025 •
edited
Loading

PR summary 7672327e9c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ contMDiffAt_zeroSection
+ contMDiffOn_zeroSection
+ contMDiffWithinAt_zeroSection

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/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).

@github-actions github-actions bot added the t-differential-geometry Manifolds etc label Jul 3, 2025
This was referenced Jul 3, 2025
Draft
Closed
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Jul 3, 2025

Would you also add ContMDiffOn and ContMDiffAt? It would feel weird to have the two extremes ContMDiff and ContMDiffWithinAt but not the middle ones.

@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 3, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jul 3, 2025

Sure!

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jul 3, 2025

Done

@grunweg grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 3, 2025
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Jul 3, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 3, 2025

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 3, 2025
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Jul 3, 2025

bors r+

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jul 3, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jul 3, 2025
@grunweg
feat: contMDiffWithinAt_zeroSection (#26676)
8615e63 
Part of the path towards geodesics and the Levi-Civita connection
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 3, 2025

Pull request successfully merged into master.

Build succeeded:

  • CI Success

@mathlib-bors mathlib-bors bot changed the title feat: contMDiffWithinAt_zeroSection [Merged by Bors] - feat: contMDiffWithinAt_zeroSection Jul 3, 2025
@mathlib-bors mathlib-bors bot closed this Jul 3, 2025
@grunweg grunweg deleted the Ckzerosection branch July 3, 2025 22:54
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Jul 7, 2025
@grunweg @joelriou
feat: contMDiffWithinAt_zeroSection (leanprover-community#26676)
a996d2f 
Part of the path towards geodesics and the Levi-Civita connection
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@grunweg @callesonne
feat: contMDiffWithinAt_zeroSection (leanprover-community#26676)
28f570f 
Part of the path towards geodesics and the Levi-Civita connection
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@grunweg @hrmacbeth
feat: contMDiffWithinAt_zeroSection (leanprover-community#26676)
136521e 
Part of the path towards geodesics and the Levi-Civita connection
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees

No one assigned

Labels

easy < 20s of review time. See the lifecycle page for guidelines. 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.

3 participants

@grunweg @sgouezel @Ruben-VandeVelde