Skip to content

[Merged by Bors] - feat: decomposition of ContinuousAffineMap as an Equiv#36083

Closed
gasparattila wants to merge 2 commits intoleanprover-community:masterfrom
gasparattila:CAM-decompEquiv
Closed

[Merged by Bors] - feat: decomposition of ContinuousAffineMap as an Equiv#36083
gasparattila wants to merge 2 commits intoleanprover-community:masterfrom
gasparattila:CAM-decompEquiv

Conversation

@gasparattila
Copy link
Copy Markdown
Contributor

@gasparattila gasparattila commented Mar 3, 2026

This PR defines an equivalence (V →ᴬ[R] Q) ≃ Q × (V →L[R] W), plus LinearEquiv and AffineEquiv variants. To match the names of the new equivalences, ContinuousAffineMap.toConstProdLinearMap is also renamed.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

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

PR summary 921b06da51

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ decompAffineEquiv
+ decompAffineEquiv_symm_apply
+ decompAffineEquiv_symm_contLinear
+ decompEquiv
+ decompEquiv_symm_apply
+ decompEquiv_symm_contLinear
+ decompLinearEquiv
+ decompLinearEquiv_symm_apply
+ decompLinearEquiv_symm_contLinear
+ decompLinearIsometryEquiv
+ decompLinearIsometryEquiv_symm_apply
+ decompLinearIsometryEquiv_symm_contLinear
+ fst_decompAffineEquiv
+ fst_decompEquiv
+ fst_decompLinearEquiv
+ fst_decompLinearIsometryEquiv
+ snd_decompAffineEquiv
+ snd_decompEquiv
+ snd_decompLinearEquiv
+ snd_decompLinearIsometryEquiv

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

@gasparattila gasparattila force-pushed the CAM-decompEquiv branch 3 times, most recently from a634b46 to ad13d3c Compare March 3, 2026 23:24
@gasparattila
feat: decomposition of ContinuousAffineMap as an Equiv
5918406 
This PR defines an equivalence `(V →ᴬ[R] Q) ≃ Q × (V →L[R] W)`, plus `LinearEquiv` and `AffineEquiv` variants. To match the names of the new equivalences, `ContinuousAffineMap.toConstProdLinearMap` is also renamed.
@gasparattila gasparattila mentioned this pull request Mar 5, 2026
Open
1 task
dupuisf
dupuisf reviewed Mar 15, 2026
View reviewed changes
@dupuisf
Copy link
Copy Markdown
Contributor

dupuisf commented Apr 1, 2026

Looks good, thanks!

bors r+

@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 1, 2026
mathlib-bors bot pushed a commit that referenced this pull request Apr 1, 2026
@gasparattila
feat: decomposition of ContinuousAffineMap as an Equiv (#36083)
23ea621 
This PR defines an equivalence `(V →ᴬ[R] Q) ≃ Q × (V →L[R] W)`, plus `LinearEquiv` and `AffineEquiv` variants. To match the names of the new equivalences, `ContinuousAffineMap.toConstProdLinearMap` is also renamed.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 1, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: decomposition of ContinuousAffineMap as an Equiv [Merged by Bors] - feat: decomposition of ContinuousAffineMap as an Equiv Apr 1, 2026
@mathlib-bors mathlib-bors bot closed this Apr 1, 2026
aditya-ramabadran pushed a commit to aditya-ramabadran/mathlib4 that referenced this pull request Apr 1, 2026
@gasparattila @aditya-ramabadran
feat: decomposition of ContinuousAffineMap as an Equiv (leanprove…
237a595 
…r-community#36083)

This PR defines an equivalence `(V →ᴬ[R] Q) ≃ Q × (V →L[R] W)`, plus `LinearEquiv` and `AffineEquiv` variants. To match the names of the new equivalences, `ContinuousAffineMap.toConstProdLinearMap` is also renamed.
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Apr 3, 2026
@gasparattila @xroblot
feat: decomposition of ContinuousAffineMap as an Equiv (leanprove…
d12e614 
…r-community#36083)

This PR defines an equivalence `(V →ᴬ[R] Q) ≃ Q × (V →L[R] W)`, plus `LinearEquiv` and `AffineEquiv` variants. To match the names of the new equivalences, `ContinuousAffineMap.toConstProdLinearMap` is also renamed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dupuisf dupuisf dupuisf left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@gasparattila @dupuisf