[Merged by Bors] - feat: transfer IsTopologicalAddGroup and ContinuousSMul across continuous linear equivalences#36435
Closed
grunweg wants to merge 17 commits intoleanprover-community:masterfrom
Closed
Conversation
PR summary aeed612d5d
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Geometry.Manifold.VectorBundle.Tensoriality | 2249 | 2252 | +3 (+0.13%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Geometry.Manifold.VectorBundle.Tensoriality |
3 |
Declarations diff
+ ContinuousLinearEquiv.continuousSMul
+ ContinuousMulEquiv.isTopologicalGroup
+ toContinuousAddEquiv
+ toContinuousAddEquiv_coe
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
…uous linear equivalences
This reverts commit 748b4c7.
8c91e83 to
2f04e1c
Compare
|
This PR/issue depends on: |
1 task
plp127
reviewed
Mar 10, 2026
ADedecker
reviewed
Mar 10, 2026
This reverts commit 791f603.
Contributor
Author
|
@ocfnash Since you asked for this change, would you like to take a look? No particular urgency on my side. |
ocfnash
reviewed
Mar 20, 2026
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
Contributor
Author
|
I consider this ready for another look. |
ocfnash
reviewed
Mar 20, 2026
ocfnash
reviewed
Mar 20, 2026
Comment on lines
+86
to
+87
| @[implicit_reducible] | ||
| def ContinuousLinearEquiv.isTopologicalAddGroup |
Contributor
There was a problem hiding this comment.
I don't understand why this is not caught by a linter but shouldn't this be:
Suggested change
| @[implicit_reducible] | |
| def ContinuousLinearEquiv.isTopologicalAddGroup | |
| lemma ContinuousLinearEquiv.isTopologicalAddGroup |
Contributor
There was a problem hiding this comment.
I wonder if instead of adding this we added ContinuousLinearEquiv.toContinuousAddEquiv. What do you think?
Contributor
Author
There was a problem hiding this comment.
That could be nicer: I just did so.
Comment on lines
+95
to
+96
| @[implicit_reducible] | ||
| def ContinuousLinearEquiv.continuousSMul |
Contributor
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] | |
| def ContinuousLinearEquiv.continuousSMul | |
| lemma ContinuousLinearEquiv.continuousSMul |
Contributor
Author
There was a problem hiding this comment.
Indeed, that looks like a linter bug: I raised it on zulip.
Contributor
|
Thanks! bors merge |
Contributor
|
Pull request successfully merged into master. Build succeeded: |
justus-springer
pushed a commit
to justus-springer/mathlib4
that referenced
this pull request
Mar 28, 2026
…uous linear equivalences (leanprover-community#36435) and use this to remove mathematically superfluous typeclass hypotheses in the tensoriality criterion. Follow-up to leanprover-community#36277/leanprover-community#36432.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
and use this to remove mathematically superfluous typeclass hypotheses in the tensoriality criterion.
Follow-up to #36277/#36432.