Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(RingTheory/EssentialFiniteness): Define essentially of finite type algebras #13162

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(RingTheory/EssentialFiniteness): Define essentially of finite type algebras #13162

wants to merge 5 commits into from

Conversation

erdOne
Copy link
Member

@erdOne erdOne commented May 24, 2024

Open in Gitpod

@erdOne erdOne added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels May 24, 2024
@erdOne @github-actions
Update Mathlib/RingTheory/EssentialFiniteness.lean
84f7796 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
chrisflav
chrisflav reviewed Jul 2, 2024
View reviewed changes
@chrisflav chrisflav added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jul 2, 2024
@erdOne erdOne added awaiting-review awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 2, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 2, 2024

PR summary 087a51ebcd

Import changes

No significant changes to the import graph

Declarations diff

+ EssFiniteType
+ EssFiniteType.adjoin_mem_finset
+ EssFiniteType.algHom_ext
+ EssFiniteType.aux
+ EssFiniteType.baseChange
+ EssFiniteType.comp
+ EssFiniteType.comp_iff
+ EssFiniteType.finset
+ EssFiniteType.isLocalization
+ EssFiniteType.of_comp
+ EssFiniteType.of_finiteType
+ EssFiniteType.of_id
+ EssFiniteType.of_isLocalization
+ EssFiniteType.submonoid
+ essFiniteType_cond_iff
+ essFiniteType_iff
+ essFiniteType_iff_exists_subalgebra
+ instance [EssFiniteType R S] : Algebra.FiniteType R (EssFiniteType.subalgebra R S) := by

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

chrisflav
chrisflav approved these changes Jul 3, 2024
View reviewed changes
Copy link
Collaborator

@chrisflav chrisflav left a comment

Choose a reason for hiding this comment

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

Thanks, looks good to me. I'll go advertise it on Zulip.

@joelriou
Copy link
Collaborator

joelriou commented Jul 6, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 6, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 6, 2024
@erdOne
feat(RingTheory/EssentialFiniteness): Define essentially of finite ty…
b9ad144 
…pe algebras (#13162)




Co-authored-by: Andrew Yang <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 6, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/EssentialFiniteness): Define essentially of finite type algebras [Merged by Bors] - feat(RingTheory/EssentialFiniteness): Define essentially of finite type algebras Jul 6, 2024
@mathlib-bors mathlib-bors bot closed this Jul 6, 2024
@mathlib-bors mathlib-bors bot deleted the erd1/essfin branch July 6, 2024 07:05
@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

@chrisflav chrisflav chrisflav 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
@erdOne @joelriou @chrisflav