[Merged by Bors] - feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm by igorkhavkine · Pull Request #25564 · leanprover-community/mathlib4

igorkhavkine · 2025-06-07T14:56:15Z

ContinuousLinearMap.coprod_comp_prodComm shows that pre-composition of a coproduct with prodComm swaps the terms in the coproduct. A dependency of #25304.

github-actions · 2025-06-07T14:57:30Z

PR summary ad4fe0ea7e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ coprod_comp_prodComm

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

Mathlib/Topology/Algebra/Module/Equiv.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

grunweg

One more round of comments: this is getting close!

Mathlib/Topology/Algebra/Module/Equiv.lean

grunweg · 2025-06-08T21:33:57Z

@YaelDillies I remember you wrote a guide about variable implicitness and explicitness (or perhaps only a sketch of what to put in it). This could be an occasion to polish that draft and get it on the webpage --- or to ask for help with that.

grunweg

Very last comments. Thanks for your patience!

Mathlib/Topology/Algebra/Module/Equiv.lean

grunweg · 2025-06-09T20:37:24Z

Let's ask a maintainer to take a look:
maintainer delegate

github-actions · 2025-06-09T20:37:45Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

fpvandoorn · 2025-06-12T10:03:04Z

bors merge

…nearEquiv.prodComm (#25564) `ContinuousLinearMap.coprod_comp_prodComm` shows that pre-composition of a coproduct with prodComm swaps the terms in the coproduct. A dependency of #25304. Co-authored-by: igorkhavkine <133780155+igorkhavkine@users.noreply.github.com>

mathlib-bors · 2025-06-12T10:15:58Z

Build failed (retrying...):

CI Success

…nearEquiv.prodComm (#25564) `ContinuousLinearMap.coprod_comp_prodComm` shows that pre-composition of a coproduct with prodComm swaps the terms in the coproduct. A dependency of #25304. Co-authored-by: igorkhavkine <133780155+igorkhavkine@users.noreply.github.com>

mathlib-bors · 2025-06-12T10:34:56Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* master: (447 commits) chore(Data/Set): move very basic lemmas earlier (leanprover-community#25707) feat: preserve draft status when migrating PRs to fork (leanprover-community#25777) chore(Data/Set/Basic): deprecate lemmas that abuse the `Set α := α → Prop` defeq (leanprover-community#25669) refactor: redefine `ProperCone` as an `abbrev` for `ClosedSubmodule` (leanprover-community#25204) feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (leanprover-community#25564) fix: outdated docstring (leanprover-community#25717) feat(MeasureTheory): convolution of measures with densities (leanprover-community#25718) feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right (leanprover-community#25604) feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948) feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (leanprover-community#25333) fix: typo in labels_from_comment.yml (leanprover-community#25727) feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705) feat: check that the mathlib options exist (leanprover-community#25687) feat(Algebra/Group/Even): Add missing lemmas (leanprover-community#20818) refactor: make `Matrix.kroneckerTMulAlgEquiv` heterogeneous (leanprover-community#25693) feat: allow contributors to remove labels with comments (leanprover-community#25723) chore: disable build.yml and bors.yml on forks (leanprover-community#25722) feat: improvements to user_activity_report.py (leanprover-community#25721) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) ...

…nearEquiv.prodComm (leanprover-community#25564) `ContinuousLinearMap.coprod_comp_prodComm` shows that pre-composition of a coproduct with prodComm swaps the terms in the coproduct. A dependency of leanprover-community#25304. Co-authored-by: igorkhavkine <133780155+igorkhavkine@users.noreply.github.com>

Added ContinuousLinearMap.coprod_comp_prodComm.

4e056f0

igorkhavkine requested review from YaelDillies and grunweg June 7, 2025 14:56

igorkhavkine added the t-analysis Analysis (normed *, calculus) label Jun 7, 2025

igorkhavkine mentioned this pull request Jun 7, 2025

feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space #25304

Closed

2 tasks

YaelDillies reviewed Jun 7, 2025

View reviewed changes

Mathlib/Topology/Algebra/Module/Equiv.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Jun 7, 2025

View reviewed changes

Mathlib/Topology/Algebra/Module/Equiv.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Algebra/Module/Equiv.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 7, 2025

Apply suggestions from code review

f0b9a81

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

grunweg reviewed Jun 8, 2025

View reviewed changes

Mathlib/Topology/Algebra/Module/Equiv.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Algebra/Module/Equiv.lean Outdated Show resolved Hide resolved

igorkhavkine added 2 commits June 9, 2025 06:53

Unsqueezed terminal simp in ContinuousLinearMap.coprod_comp_prodComm.

cb59e55

Cleaned up comments.

958ad4d

igorkhavkine removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 9, 2025

grunweg reviewed Jun 9, 2025

View reviewed changes

Mathlib/Topology/Algebra/Module/Equiv.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Algebra/Module/Equiv.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Algebra/Module/Equiv.lean Outdated Show resolved Hide resolved

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 9, 2025

grunweg changed the title ~~feat(Topology/Algebra/Module): interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm~~ feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm Jun 9, 2025

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 9, 2025

grunweg added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jun 9, 2025

igorkhavkine and others added 2 commits June 10, 2025 22:30

Apply suggestions from code review

2e752ab

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

Merge branch 'master' into igorkhavkine/clm_coprod_prodComm

11ecec9

igorkhavkine added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 10, 2025

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 10, 2025

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 Jun 12, 2025

mathlib-bors bot changed the title ~~feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm~~ [Merged by Bors] - feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm Jun 12, 2025

mathlib-bors bot closed this Jun 12, 2025

mathlib-bors bot deleted the igorkhavkine/clm_coprod_prodComm branch June 12, 2025 10:35

igorkhavkine mentioned this pull request Jun 23, 2025

feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space #26300

Open

2 tasks

Conversation

igorkhavkine commented Jun 7, 2025 • edited by grunweg Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ad4fe0ea7e

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jun 8, 2025

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Jun 9, 2025

Uh oh!

github-actions bot commented Jun 9, 2025

Uh oh!

fpvandoorn commented Jun 12, 2025

Uh oh!

mathlib-bors bot commented Jun 12, 2025

Uh oh!

mathlib-bors bot commented Jun 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

igorkhavkine commented Jun 7, 2025 •

edited by grunweg

Loading

github-actions bot commented Jun 7, 2025 •

edited

Loading