Skip to content

[Merged by Bors] - feat(Algebra/Star/NonUnitalSubsemiring): Add NonUnitalStarSubsemiring#12938

Closed
mans0954 wants to merge 35 commits intomasterfrom
mans0954/StarSubSemiring
Closed

[Merged by Bors] - feat(Algebra/Star/NonUnitalSubsemiring): Add NonUnitalStarSubsemiring#12938
mans0954 wants to merge 35 commits intomasterfrom
mans0954/StarSubSemiring

Conversation

@mans0954
Copy link
Copy Markdown
Collaborator

@mans0954 mans0954 commented May 15, 2024

Definitions and basic properties of non-unital star subsemirings

This file heavily copies Mathlib.Algebra.Star.NonUnitalSubalgebra, so I'm happy to assign the copyright to @j-loreaux if that's the appropriate thing to do.

So far I've mostly only developed what's required for #6595 - I thought I'd check that this was the right approach before going further.

Open in Gitpod

@mans0954 mans0954 mentioned this pull request May 15, 2024
Closed
3 tasks
@j-loreaux j-loreaux self-assigned this May 19, 2024
j-loreaux
j-loreaux reviewed May 19, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

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

I think we don't want StarSubset, unless you have an explicit application in mind. Also, it would be nice if the unital versions of all these were placed in a separate file.

@j-loreaux j-loreaux added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels May 19, 2024
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented May 19, 2024

no need to include me in the copyright.

github-actions[bot]
github-actions bot reviewed Jun 4, 2024
View reviewed changes
@mans0954 mans0954 added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 4, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

Import summary

No significant changes to the import graph

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 15, 2024 •
edited
Loading

PR summary f3295abb61

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Star.NonUnitalSubsemiring 572
Mathlib.Algebra.Star.Subsemiring 584

Declarations diff

+ NonUnitalStarSubsemiring
+ StarSubsemiring
+ SubStarSemigroup
+ coe_mk
+ coe_toSubsemiring
+ ext
+ instNonUnitalSubsemiringClass
+ instSetLike
+ instStarMemClass
+ mem_toSubsemiring
+ semiring
+ setLike
+ starMemClass
+ starRing
+ subsemiringClass
+ toSubsemiring_inj
+ toSubsemiring_injective
+ toSubsemiring_le_iff
++ coe_copy
++ copy
++ copy_eq
++ mem_carrier
+++ center

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>

@mans0954 mans0954 added the t-algebra Algebra (groups, rings, fields, etc) label Jul 14, 2024
j-loreaux
j-loreaux approved these changes Jul 15, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

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

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 15, 2024

✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 15, 2024
@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Jul 15, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jul 15, 2024
@mans0954
feat(Algebra/Star/NonUnitalSubsemiring): Add NonUnitalStarSubsemiring (…
a67c141 
…#12938)

Definitions and basic properties of non-unital star subsemirings



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
mathlib-bors bot pushed a commit that referenced this pull request Jul 15, 2024
@mans0954
feat(Algebra/Star/NonUnitalSubsemiring): Add NonUnitalStarSubsemiring (…
cb0404f 
…#12938)

Definitions and basic properties of non-unital star subsemirings



Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 15, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Star/NonUnitalSubsemiring): Add NonUnitalStarSubsemiring [Merged by Bors] - feat(Algebra/Star/NonUnitalSubsemiring): Add NonUnitalStarSubsemiring Jul 15, 2024
@mathlib-bors mathlib-bors bot closed this Jul 15, 2024
@mathlib-bors mathlib-bors bot deleted the mans0954/StarSubSemiring branch July 15, 2024 21:07
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@github-actions github-actions[bot] github-actions[bot] left review comments

@j-loreaux j-loreaux j-loreaux approved these changes

Assignees

@j-loreaux j-loreaux

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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

@mans0954 @j-loreaux @kim-em