Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - refactor(field_theory/polynomial_galois_group): remove open_locale classical#19184

Closed
eric-wieser wants to merge 1 commit intomasterfrom
eric-wieser/more-classical
Closed

[Merged by Bors] - refactor(field_theory/polynomial_galois_group): remove open_locale classical#19184
eric-wieser wants to merge 1 commit intomasterfrom
eric-wieser/more-classical

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Jun 13, 2023 •
edited
Loading

This doesn't actually generalize any lemmas, but it reduces the chance of lemmas added in future being less general.

The restrict_dvd_def lemma is new, and deals with substituting an arbitray decidable_eq instance.

Open in Gitpod

@eric-wieser eric-wieser added the WIP Work in progress label Jun 13, 2023
@riccardobrasca riccardobrasca mentioned this pull request Jun 14, 2023
Closed
3 tasks
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jun 14, 2023 •
edited
Loading

This is clearly an improvement. Can you just update the description of the PR?

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Jun 14, 2023

Thanks 🎉

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Jun 14, 2023

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

@github-actions github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label Jun 14, 2023
@eric-wieser eric-wieser changed the title refactor(field_theory/polynomial_galois_group): remove `open_locale c… refactor(field_theory/polynomial_galois_group): remove open_locale classical Jun 14, 2023
@eric-wieser
Copy link
Copy Markdown
Member Author

eric-wieser commented Jun 14, 2023

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Jun 14, 2023

👎 Rejected by label

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jun 14, 2023
@riccardobrasca riccardobrasca removed the WIP Work in progress label Jun 14, 2023
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jun 14, 2023

bors merge

ericrbg
ericrbg approved these changes Jun 14, 2023
View reviewed changes
Copy link
Copy Markdown
Collaborator

@ericrbg ericrbg left a comment

Choose a reason for hiding this comment

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

otherwise lgtm

src/field_theory/polynomial_galois_group.lean
lemma restrict_dvd_surjective (hpq : p ∣ q) (hq : q ≠ 0) :
function.surjective (restrict_dvd hpq) :=
by simp only [restrict_dvd, dif_neg hq, restrict_surjective]
by classical; simp only [restrict_dvd_def, dif_neg hq, restrict_surjective]
Copy link
Copy Markdown
Collaborator

@ericrbg ericrbg Jun 14, 2023

Choose a reason for hiding this comment

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

Suggested change
by classical; simp only [restrict_dvd_def, dif_neg hq, restrict_surjective]
by { classical, simp only [restrict_dvd_def, dif_neg hq, restrict_surjective] }

I prefer the original style but I think this is discouraged? I guess it won't matter in Lean4

Copy link
Copy Markdown
Collaborator

@ericrbg ericrbg Jun 14, 2023

Choose a reason for hiding this comment

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

oh I see that this PR is already bors'd - pls ignore

bors bot pushed a commit that referenced this pull request Jun 14, 2023
@eric-wieser
refactor(field_theory/polynomial_galois_group): remove `open_locale c…
8bdf5e9 
…lassical` (#19184)

This doesn't actually generalize any lemmas, but it reduces the chance of lemmas added in future being less general.

The `restrict_dvd_def` lemma is new, and deals with substituting an arbitray `decidable_eq` instance.
@bors
Copy link
Copy Markdown

bors bot commented Jun 14, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title refactor(field_theory/polynomial_galois_group): remove open_locale classical [Merged by Bors] - refactor(field_theory/polynomial_galois_group): remove open_locale classical Jun 14, 2023
@bors bors bot closed this Jun 14, 2023
@bors bors bot deleted the eric-wieser/more-classical branch June 14, 2023 15:43
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@ericrbg ericrbg ericrbg approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@eric-wieser @riccardobrasca @jcommelin @ericrbg