Skip to content

[Merged by Bors] - feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ and quotientEquivOfIsTopCompl_comp_mkQ#39613

Closed
sharky564 wants to merge 9 commits into
leanprover-community:masterfrom
sharky564:SK_quotientEquiv_comp_mkQ
Closed

[Merged by Bors] - feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ and quotientEquivOfIsTopCompl_comp_mkQ#39613
sharky564 wants to merge 9 commits into
leanprover-community:masterfrom
sharky564:SK_quotientEquiv_comp_mkQ

Conversation

@sharky564

@sharky564 sharky564 commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Adds the lemmas Submodule.quotientEquivOfIsCompl_comp_mkQ and quotientEquivOfIsTopCompl_comp_mkQ - the composition of quotientEquivOfIsCompl/quotientEquivOfIsTopCompl with mkQ agrees with the linear projection onto q along p. Additionally the proof of IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl is simplified.

This lemma was flagged as missing in the API in the review of #39260 by @themathqueen. Upon review of the lemma, I found it could be further simplified.

@github-actions

github-actions Bot commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 6e69f7f4a9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ quotientEquivOfIsCompl_comp_mkQ
+ quotientEquivOfIsTopCompl_comp_mkQL

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 6e69f7f4a9
Reference commit 185c8cd930

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

@github-actions github-actions Bot added t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters labels May 21, 2026
ADedecker
ADedecker reviewed May 23, 2026
View reviewed changes
Comment thread Mathlib/LinearAlgebra/Projection.lean Outdated
Comment thread Mathlib/LinearAlgebra/Projection.lean Outdated
Comment thread Mathlib/Topology/Algebra/Module/Complement.lean Outdated
@ADedecker ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes. label May 23, 2026
@sharky564 sharky564 changed the title feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ and quotientEquivOfIsTopCompl_comp_mkQ May 24, 2026
@sharky564

sharky564 commented May 24, 2026

Copy link
Copy Markdown
Contributor Author

I've updated the PR with these.
-awaiting-author

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 24, 2026
themathqueen
themathqueen reviewed May 24, 2026
View reviewed changes
Comment thread Mathlib/Topology/Algebra/Module/Complement.lean Outdated
@sharky564 @themathqueen
Update Mathlib/Topology/Algebra/Module/Complement.lean
5988482 
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
@sharky564

sharky564 commented May 28, 2026

Copy link
Copy Markdown
Contributor Author

@ADedecker @themathqueen we should be good to merge this

themathqueen
themathqueen reviewed Jun 2, 2026
View reviewed changes
Comment thread Mathlib/Topology/Algebra/Module/Complement.lean Outdated
@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 3, 2026
@sharky564 @themathqueen
Update Mathlib/Topology/Algebra/Module/Complement.lean
c16dd59 
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
@ADedecker ADedecker removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 3, 2026
@ADedecker

ADedecker commented Jun 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

Sorry for the delay, and thanks for your contribution! You can merge after fixing the CI failure.

bors d+

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Jun 3, 2026
@ADedecker

ADedecker commented Jun 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

Did something stupid (I'm tired).

bors cancel

@mathlib-bors

mathlib-bors Bot commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

✌️ sharky564 can now approve this pull request until 2026-06-17 15:37 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

@mathlib-bors

mathlib-bors Bot commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

Canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

@ADedecker

ADedecker commented Jun 3, 2026

Copy link
Copy Markdown
Member

bors d+

@mathlib-bors

mathlib-bors Bot commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

✌️ sharky564 can now approve this pull request until 2026-06-17 15:38 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jun 3, 2026
@ADedecker ADedecker removed the ready-to-merge This PR has been sent to bors. label Jun 3, 2026
@sharky564

sharky564 commented Jun 3, 2026

Copy link
Copy Markdown
Contributor Author

bors r+

themathqueen
themathqueen reviewed Jun 3, 2026
View reviewed changes
Comment thread Mathlib/Topology/Algebra/Module/Complement.lean Outdated
@themathqueen

themathqueen commented Jun 3, 2026

Copy link
Copy Markdown
Collaborator

You forgot to update the name! Can I cancel bors?
bors r-

@mathlib-bors

mathlib-bors Bot commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

🔒 Permission denied

Existing reviewers: click here to make themathqueen a reviewer

@sharky564

sharky564 commented Jun 3, 2026

Copy link
Copy Markdown
Contributor Author

bors r-

@mathlib-bors

mathlib-bors Bot commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

Canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

@sharky564 @themathqueen
Update Mathlib/Topology/Algebra/Module/Complement.lean
6e69f7f 
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
@sharky564

sharky564 commented Jun 3, 2026

Copy link
Copy Markdown
Contributor Author

bors r+

mathlib-bors Bot pushed a commit that referenced this pull request Jun 3, 2026
@sharky564
feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ a…
dd27355 
…nd quotientEquivOfIsTopCompl_comp_mkQ (#39613)

Adds the lemmas `Submodule.quotientEquivOfIsCompl_comp_mkQ` and `quotientEquivOfIsTopCompl_comp_mkQ` - the composition of `quotientEquivOfIsCompl`/`quotientEquivOfIsTopCompl` with `mkQ` agrees with the linear projection onto `q`  along `p`. Additionally the proof of `IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl` is simplified.
@mathlib-bors

mathlib-bors Bot commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ and quotientEquivOfIsTopCompl_comp_mkQ [Merged by Bors] - feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ and quotientEquivOfIsTopCompl_comp_mkQ Jun 3, 2026
@mathlib-bors mathlib-bors Bot closed this Jun 3, 2026
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@sharky564 @Bergschaf
feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ a…
81291d4 
…nd quotientEquivOfIsTopCompl_comp_mkQ (leanprover-community#39613)

Adds the lemmas `Submodule.quotientEquivOfIsCompl_comp_mkQ` and `quotientEquivOfIsTopCompl_comp_mkQ` - the composition of `quotientEquivOfIsCompl`/`quotientEquivOfIsTopCompl` with `mkQ` agrees with the linear projection onto `q`  along `p`. Additionally the proof of `IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl` is simplified.
ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026
@sharky564 @ReemMelamed
feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ a…
76923f0 
…nd quotientEquivOfIsTopCompl_comp_mkQ (leanprover-community#39613)

Adds the lemmas `Submodule.quotientEquivOfIsCompl_comp_mkQ` and `quotientEquivOfIsTopCompl_comp_mkQ` - the composition of `quotientEquivOfIsCompl`/`quotientEquivOfIsTopCompl` with `mkQ` agrees with the linear projection onto `q`  along `p`. Additionally the proof of `IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl` is simplified.
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
@ADedecker ADedecker ADedecker left review comments

Assignees

@jcommelin jcommelin

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc) 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.

5 participants

@sharky564 @ADedecker @themathqueen @jcommelin @j-loreaux