Skip to content

[Merged by Bors] - feat(Algebra): exactness lemma for linear map#36980

Closed
Thmoas-Guan wants to merge 6 commits intoleanprover-community:masterfrom
Thmoas-Guan:exactness-lemma
Closed

[Merged by Bors] - feat(Algebra): exactness lemma for linear map#36980
Thmoas-Guan wants to merge 6 commits intoleanprover-community:masterfrom
Thmoas-Guan:exactness-lemma

Conversation

@Thmoas-Guan
Copy link
Copy Markdown
Collaborator

@Thmoas-Guan Thmoas-Guan commented Mar 22, 2026

Add some variant of existing lemma for linear map

Open in Gitpod

@Thmoas-Guan Thmoas-Guan mentioned this pull request Mar 22, 2026
Open
1 task
@github-actions
Copy link
Copy Markdown

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

PR summary 6ef8cc2731

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ LinearEquiv.conj_symm_exact_iff_exact
+ _root_.LinearEquiv.postcomp_exact_iff_exact
+ _root_.LinearEquiv.precomp_exact_iff_exact

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

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Mar 22, 2026
WilliamCoram
WilliamCoram reviewed Mar 31, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Exact.lean Outdated
WilliamCoram
WilliamCoram reviewed Mar 31, 2026
View reviewed changes
Comment thread Mathlib/Algebra/Exact.lean Outdated
dagurtomas
dagurtomas reviewed Apr 2, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas left a comment

Choose a reason for hiding this comment

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

I'm not entirely sure about the names here, but fst and snd usually refer to projections from something like a product. I suggest precomp and postcomp, but those names don't describe whether it's the first or the second map that is being composed with, so not ideal either. Another option would be to replace fst/snd with left/right.

maintainer delegate

Comment thread Mathlib/Algebra/Exact.lean Outdated
Comment thread Mathlib/Algebra/Exact.lean Outdated
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 2, 2026

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

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 2, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Apr 4, 2026

Thanks!

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Apr 4, 2026
@Thmoas-Guan
feat(Algebra): exactness lemma for linear map (#36980)
3bb1afa 
Add some variant of existing lemma for linear map
@mathlib-triage mathlib-triage bot 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 Apr 4, 2026
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 4, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra): exactness lemma for linear map [Merged by Bors] - feat(Algebra): exactness lemma for linear map Apr 4, 2026
@mathlib-bors mathlib-bors bot closed this Apr 4, 2026
riccardobrasca pushed a commit to riccardobrasca/mathlib4 that referenced this pull request Apr 6, 2026
@Thmoas-Guan @riccardobrasca
feat(Algebra): exactness lemma for linear map (leanprover-community#3…
a5544fa 
…6980)

Add some variant of existing lemma for linear map
YellPika pushed a commit to YellPika/mathlib4 that referenced this pull request Apr 6, 2026
@Thmoas-Guan @YellPika
feat(Algebra): exactness lemma for linear map (leanprover-community#3…
355af00 
…6980)

Add some variant of existing lemma for linear map
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dagurtomas dagurtomas dagurtomas left review comments

+1 more reviewer

@WilliamCoram WilliamCoram WilliamCoram left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@dagurtomas dagurtomas

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@Thmoas-Guan @riccardobrasca @dagurtomas @WilliamCoram