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(ring_theory/{trace,norm}): add trace_gen_eq_next_coeff_minpoly and norm_gen_eq_coeff_zero_minpoly #11420

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat(ring_theory/{trace,norm}): add trace_gen_eq_next_coeff_minpoly and norm_gen_eq_coeff_zero_minpoly #11420

wants to merge 14 commits into from

Conversation

riccardobrasca
Copy link
Member

@riccardobrasca riccardobrasca commented Jan 13, 2022 •
edited

We add trace_gen_eq_next_coeff_minpoly and norm_gen_eq_coeff_zero_minpoly.

From flt-regular.

Open in Gitpod

@riccardobrasca riccardobrasca added the awaiting-review The author would like community review of the PR label Jan 13, 2022
@Vierkantor Vierkantor changed the title refacor(ring_theory/norm): add norm_gen_eq_coeff_zero_minpoly refactor(ring_theory/norm): add norm_gen_eq_coeff_zero_minpoly Jan 13, 2022
Vierkantor
Vierkantor reviewed Jan 13, 2022
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Could you do the same for trace and the degree p - 1th coefficient of a polynomial p?

src/ring_theory/norm.lean Outdated Show resolved Hide resolved
src/ring_theory/norm.lean Outdated Show resolved Hide resolved
src/field_theory/splitting_field.lean Outdated Show resolved Hide resolved
@Vierkantor Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jan 13, 2022
riccardobrasca and others added 4 commits January 13, 2022 12:00
@riccardobrasca @Vierkantor
Update src/ring_theory/norm.lean
86a3cb8 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@riccardobrasca @Vierkantor
Update src/ring_theory/norm.lean
11a74e9 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@riccardobrasca @Vierkantor
Update src/field_theory/splitting_field.lean
b5a7f7b 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@riccardobrasca
fix build
077ce71
@riccardobrasca riccardobrasca changed the title refactor(ring_theory/norm): add norm_gen_eq_coeff_zero_minpoly feat(ring_theory/norm): add norm_gen_eq_coeff_zero_minpoly Jan 13, 2022
@riccardobrasca riccardobrasca changed the title feat(ring_theory/norm): add norm_gen_eq_coeff_zero_minpoly feat(ring_theory/{trace,norm}): add power_basis.trace_gen_eq_next_coeff_minpoly and power_basis.norm_gen_eq_coeff_zero_minpoly Jan 13, 2022
@riccardobrasca riccardobrasca changed the title feat(ring_theory/{trace,norm}): add power_basis.trace_gen_eq_next_coeff_minpoly and power_basis.norm_gen_eq_coeff_zero_minpoly feat(ring_theory/{trace,norm}): add trace_gen_eq_next_coeff_minpoly and norm_gen_eq_coeff_zero_minpoly Jan 13, 2022
@riccardobrasca
Copy link
Member Author

Could you do the same for trace and the degree p - 1th coefficient of a polynomial p?

Done. I've also modified the name of norm_gen_eq_prod_roots, that is now power_basis.norm_gen_eq_prod_roots, to be consistent with the trace case. (I can of course go the other way if it's better.)

@riccardobrasca riccardobrasca added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 13, 2022
Vierkantor
Vierkantor approved these changes Jan 13, 2022
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor 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 r+

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jan 13, 2022
@bors
Copy link

bors bot commented Jan 13, 2022

Canceled.

@riccardobrasca
Copy link
Member Author

riccardobrasca commented Jan 13, 2022 •
edited

I pushed a fix (just an unused argument). @Vierkantor can you delegate me please? I will merge once CI passes. Thanks!

@Vierkantor
Copy link
Collaborator

Sure thing!

bors d+

@bors
Copy link

bors bot commented Jan 13, 2022

✌️ riccardobrasca 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 Jan 13, 2022
@riccardobrasca
Copy link
Member Author

bors r+

bors bot pushed a commit that referenced this pull request Jan 13, 2022
@riccardobrasca
feat(ring_theory/{trace,norm}): add trace_gen_eq_next_coeff_minpoly a…
6446ba8 
…nd norm_gen_eq_coeff_zero_minpoly (#11420)

We add `trace_gen_eq_next_coeff_minpoly` and `norm_gen_eq_coeff_zero_minpoly`.

From flt-regular.
@bors
Copy link

bors bot commented Jan 13, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/{trace,norm}): add trace_gen_eq_next_coeff_minpoly and norm_gen_eq_coeff_zero_minpoly [Merged by Bors] - feat(ring_theory/{trace,norm}): add trace_gen_eq_next_coeff_minpoly and norm_gen_eq_coeff_zero_minpoly Jan 13, 2022
@bors bors bot closed this Jan 13, 2022
@bors bors bot deleted the RB/norm_lemma branch January 13, 2022 17:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Vierkantor approved these changes

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.

None yet
3 participants
@riccardobrasca @Vierkantor @leanprover-community-bot-assistant