Skip to content

[Merged by Bors] - chore: move Pretrivialization, Trivialization to the Bundle namespace#31338

Closed
grunweg wants to merge 3 commits intoleanprover-community:masterfrom
grunweg:rename-triv
Closed

[Merged by Bors] - chore: move Pretrivialization, Trivialization to the Bundle namespace#31338
grunweg wants to merge 3 commits intoleanprover-community:masterfrom
grunweg:rename-triv

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Nov 7, 2025 •
edited
Loading

@grunweg grunweg added the t-differential-geometry Manifolds etc label Nov 7, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 7, 2025 •
edited
Loading

PR summary 91fb523cd9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Bundle.Pretrivialization
+ Bundle.Pretrivialization.IsLinear
+ Bundle.Trivialization,
+ Bundle.Trivialization.baseSet_continuousLinearMap
+ Bundle.Trivialization.contMDiffOn_symm_trans
+ Bundle.Trivialization.contMDiffWithinAt_snd_comp_iff₂
+ Bundle.Trivialization.continuousLinearEquivAt_prod
+ Bundle.Trivialization.continuousLinearMap
+ Bundle.Trivialization.continuousLinearMap_apply
+ Bundle.Trivialization.mdifferentiable
+ Bundle.Trivialization.pullback
+ Bundle.Trivialization.pullback_linear
+ contMDiffAt_iff
+ contMDiffAt_section_iff
+ contMDiffOn
+ contMDiffOn_iff
+ contMDiffOn_section_baseSet_iff
+ contMDiffOn_section_iff
+ contMDiffOn_symm
+ contMDiffWithinAt_iff
+ contMDiffWithinAt_section
+ contMDiff_iff
+ mdifferentiableAt_section_iff
+ mdifferentiableAt_snd_comp_iff₂
+ mdifferentiableAt_totalSpace_iff
+ mdifferentiableOn_section_baseSet_iff
+ mdifferentiableOn_section_iff
+ mdifferentiableWithinAt_section_iff
+ mdifferentiableWithinAt_snd_comp_iff₂
+ mdifferentiableWithinAt_totalSpace_iff
- Pretrivialization
- Pretrivialization.IsLinear
- Trivialization.baseSet_continuousLinearMap
- Trivialization.contMDiffAt_iff
- Trivialization.contMDiffAt_section_iff
- Trivialization.contMDiffOn
- Trivialization.contMDiffOn_iff
- Trivialization.contMDiffOn_section_baseSet_iff
- Trivialization.contMDiffOn_section_iff
- Trivialization.contMDiffOn_symm
- Trivialization.contMDiffOn_symm_trans
- Trivialization.contMDiffWithinAt_iff
- Trivialization.contMDiffWithinAt_section
- Trivialization.contMDiffWithinAt_snd_comp_iff₂
- Trivialization.contMDiff_iff
- Trivialization.continuousLinearEquivAt_prod
- Trivialization.continuousLinearMap
- Trivialization.continuousLinearMap_apply
- Trivialization.mdifferentiable
- Trivialization.mdifferentiableAt_section_iff
- Trivialization.mdifferentiableAt_snd_comp_iff₂
- Trivialization.mdifferentiableAt_totalSpace_iff
- Trivialization.mdifferentiableOn_section_baseSet_iff
- Trivialization.mdifferentiableOn_section_iff
- Trivialization.mdifferentiableWithinAt_section_iff
- Trivialization.mdifferentiableWithinAt_snd_comp_iff₂
- Trivialization.mdifferentiableWithinAt_totalSpace_iff
- Trivialization.pullback
- Trivialization.pullback_linear

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

@grunweg grunweg mentioned this pull request Nov 7, 2025
Closed
1 task
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 7, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 19, 2025

This pull request has conflicts, please merge master and resolve them.

@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 24, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Feb 24, 2026

This PR/issue depends on:

@grunweg grunweg added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 27, 2026
@grunweg grunweg requested a review from ocfnash February 27, 2026 15:49
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 27, 2026
@ocfnash
Copy link
Copy Markdown
Contributor

ocfnash commented Feb 27, 2026

Thanks!

bors merge

@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Feb 27, 2026
mathlib-bors bot pushed a commit that referenced this pull request Feb 27, 2026
@grunweg
chore: move Pretrivialization, Trivialization to the Bundle namespace (…
fd11b7a 
…#31338)

As suggested in #30083.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 27, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: move Pretrivialization, Trivialization to the Bundle namespace [Merged by Bors] - chore: move Pretrivialization, Trivialization to the Bundle namespace Feb 27, 2026
@mathlib-bors mathlib-bors bot closed this Feb 27, 2026
@grunweg grunweg deleted the rename-triv branch February 28, 2026 15:52
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Mar 2, 2026
@grunweg @pfaffelh
chore: move Pretrivialization, Trivialization to the Bundle namespace (…
1270b0d 
…leanprover-community#31338)

As suggested in leanprover-community#30083.
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026
@grunweg @xroblot
chore: move Pretrivialization, Trivialization to the Bundle namespace (…
0000340 
…leanprover-community#31338)

As suggested in leanprover-community#30083.
pevogam pushed a commit to pevogam/mathlib4 that referenced this pull request Mar 19, 2026
@grunweg @pevogam
chore: move Pretrivialization, Trivialization to the Bundle namespace (…
7b80cb6 
…leanprover-community#31338)

As suggested in leanprover-community#30083.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ocfnash ocfnash Awaiting requested review from ocfnash

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

@grunweg @mathlib4-merge-conflict-bot @ocfnash @mathlib4-dependent-issues-bot