Skip to content

[Merged by Bors] - feat(RingTheory/RingHomProperties): constructors for conjunctions#24375

Closed
chrisflav wants to merge 4 commits intomasterfrom
chrisflav-ringhomprop-and
Closed

[Merged by Bors] - feat(RingTheory/RingHomProperties): constructors for conjunctions#24375
chrisflav wants to merge 4 commits intomasterfrom
chrisflav-ringhomprop-and

Conversation

@chrisflav
Copy link
Copy Markdown
Member

@chrisflav chrisflav commented Apr 25, 2025

Open in Gitpod

@chrisflav chrisflav added the t-algebra Algebra (groups, rings, fields, etc) label Apr 25, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 25, 2025 •
edited
Loading

PR summary f48aef20ec

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsStableUnderBaseChange.and
+ RespectsIso.and
+ RingHom.LocalizationAwayPreserves.and
+ RingHom.OfLocalizationSpan.and
+ RingHom.OfLocalizationSpanTarget.and
+ RingHom.PropertyIsLocal.and
+ RingHom.StableUnderCompositionWithLocalizationAwayTarget.and
+ StableUnderComposition.and

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

erdOne
erdOne reviewed Apr 27, 2025
View reviewed changes
@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 27, 2025
chrisflav and others added 2 commits May 1, 2025 14:08
@chrisflav @erdOne
Update Mathlib/RingTheory/RingHomProperties.lean
0c2a9ef 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@chrisflav
fix
bcf51bf
@chrisflav chrisflav 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 May 1, 2025
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 1, 2025
@chrisflav chrisflav mentioned this pull request May 1, 2025
Closed
1 task
@chrisflav
Copy link
Copy Markdown
Member Author

chrisflav commented May 9, 2025

Anything else I should change here @erdOne ?

erdOne
erdOne approved these changes May 9, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

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

Nothing!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented May 9, 2025

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 9, 2025
riccardobrasca
riccardobrasca approved these changes May 10, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca 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 ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 10, 2025
mathlib-bors bot pushed a commit that referenced this pull request May 10, 2025
@chrisflav
feat(RingTheory/RingHomProperties): constructors for conjunctions (#2…
b4deda0 
…4375)

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 10, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/RingHomProperties): constructors for conjunctions [Merged by Bors] - feat(RingTheory/RingHomProperties): constructors for conjunctions May 10, 2025
@mathlib-bors mathlib-bors bot closed this May 10, 2025
@mathlib-bors mathlib-bors bot deleted the chrisflav-ringhomprop-and branch May 10, 2025 09:48
tannerduve pushed a commit that referenced this pull request May 13, 2025
@chrisflav @tannerduve
feat(RingTheory/RingHomProperties): constructors for conjunctions (#2…
7197734 
…4375)

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
bwehlin pushed a commit to bwehlin/mathlib4 that referenced this pull request May 31, 2025
@chrisflav
feat(RingTheory/RingHomProperties): constructors for conjunctions (le…
4f8dc9f 
…anprover-community#24375)

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@riccardobrasca riccardobrasca riccardobrasca approved these changes

@erdOne erdOne erdOne approved these changes

Assignees

No one assigned

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.

3 participants

@chrisflav @riccardobrasca @erdOne