Skip to content

[Merged by Bors] - feat: add ContinuousLinearEquiv.prodProdProdComm#28840

Closed
grunweg wants to merge 1 commit intoleanprover-community:masterfrom
grunweg:cle-prodprodprodcomm
Closed

[Merged by Bors] - feat: add ContinuousLinearEquiv.prodProdProdComm#28840
grunweg wants to merge 1 commit intoleanprover-community:masterfrom
grunweg:cle-prodprodprodcomm

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Aug 24, 2025 •
edited
Loading

In analogy to LinearEquiv.prodProdProdComm.

From the path towards smooth immersions, embeddings and embedded submanifolds.

Open in Gitpod

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Aug 24, 2025

@ocfnash Would you like to review this? Otherwise, I can also ask Eric (but I figure he has many reviews on his plate already).

@github-actions github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Aug 24, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 24, 2025

PR summary 0611ded866

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ coe_prodProdProdComm
+ prodProdProdComm
+ prodProdProdComm_apply
+ prodProdProdComm_symm
+ prodProdProdComm_toLinearEquiv

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

themathqueen
themathqueen reviewed Aug 24, 2025
View reviewed changes
Mathlib/Topology/Algebra/Module/Equiv.lean
rfl

@[simp]
lemma prodProdProdComm_toLinearEquiv :
Copy link
Copy Markdown
Collaborator

@themathqueen themathqueen Aug 24, 2025

Choose a reason for hiding this comment

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

Suggested change
lemma prodProdProdComm_toLinearEquiv :
lemma toLinearEquiv_prodProdProdComm :

Copy link
Copy Markdown
Contributor

@ocfnash ocfnash Aug 24, 2025

Choose a reason for hiding this comment

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

I believe @themathqueen is technically correct here but we're quite consistently inconsistent with our own naming when dot notation gets involved (for a similar case, see LinearEquiv.prodProdProdComm_toAddEquiv) so I think I advocate leaving this as-is.

Probably one day we should think more carefully about this.

Copy link
Copy Markdown
Contributor Author

@grunweg grunweg Aug 24, 2025

Choose a reason for hiding this comment

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

Indeed, I adapted the naming of the LinearEquiv analogue. I agree with you on both counts; today is not the day I'm going to review all the names.

@ocfnash ocfnash self-assigned this Aug 24, 2025
@grunweg grunweg mentioned this pull request Aug 24, 2025
Closed
3 tasks
ocfnash
ocfnash approved these changes Aug 24, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Aug 24, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Aug 24, 2025

Thanks for the quick review, this is great!

mathlib-bors bot pushed a commit that referenced this pull request Aug 24, 2025
@grunweg
feat: add ContinuousLinearEquiv.prodProdProdComm (#28840)
6f1af37 
In analogy to `LinearEquiv.prodProdProdComm`.

From the path towards smooth immersions, embeddings and embedded submanifolds.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 24, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: add ContinuousLinearEquiv.prodProdProdComm [Merged by Bors] - feat: add ContinuousLinearEquiv.prodProdProdComm Aug 24, 2025
@mathlib-bors mathlib-bors bot closed this Aug 24, 2025
YaelDillies pushed a commit to YaelDillies/mathlib4 that referenced this pull request Aug 24, 2025
@grunweg @YaelDillies
feat: add ContinuousLinearEquiv.prodProdProdComm (leanprover-communit…
4ca189a 
…y#28840)

In analogy to `LinearEquiv.prodProdProdComm`.

From the path towards smooth immersions, embeddings and embedded submanifolds.
@grunweg grunweg deleted the cle-prodprodprodcomm branch August 24, 2025 13:04
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@grunweg @pechersky
feat: add ContinuousLinearEquiv.prodProdProdComm (leanprover-communit…
292bcd2 
…y#28840)

In analogy to `LinearEquiv.prodProdProdComm`.

From the path towards smooth immersions, embeddings and embedded submanifolds.
FormulaRabbit81 pushed a commit to YaelDillies/mathlib4 that referenced this pull request Aug 30, 2025
@grunweg @FormulaRabbit81
feat: add ContinuousLinearEquiv.prodProdProdComm (leanprover-communit…
15446dd 
…y#28840)

In analogy to `LinearEquiv.prodProdProdComm`.

From the path towards smooth immersions, embeddings and embedded submanifolds.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@themathqueen themathqueen themathqueen left review comments

@ocfnash ocfnash ocfnash approved these changes

Assignees

@ocfnash ocfnash

Labels

ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@grunweg @ocfnash @themathqueen