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/power_basis): minpoly_gen is always the minimal polynomial #18117

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial #18117

wants to merge 12 commits into from

Conversation

alreadydone
Copy link
Collaborator

@alreadydone alreadydone commented Jan 10, 2023 •
edited

  • add minpoly.unique', a characterization for being the minimal polynomial.

  • golf various proofs and remove some unnecessary typeclass assumptions.

Open in Gitpod

@alreadydone alreadydone added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Jan 10, 2023
@alreadydone
Copy link
Collaborator Author

@Paul-Lez since you're working on minimal polynomials, maybe you'd be interested in the new developments here. I'm also planning to introduce a has_proper_minpoly predicate for an element saying that the annihilating ideal is generated by a single monic element, and prove equivalent characterizations such as the existence of a polynomial satisfying the hypotheses of minpoly.unique'.

@alreadydone alreadydone 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 10, 2023
@Paul-Lez
Copy link
Collaborator

@Paul-Lez since you're working on minimal polynomials, maybe you'd be interested in the new developments here. I'm also planning to introduce a has_proper_minpoly predicate for an element saying that the annihilating ideal is generated by a single monic element, and prove equivalent characterizations such as the existence of a polynomial satisfying the hypotheses of minpoly.unique'.

Oh nice, thanks for keeping me posted! Hopefully #18021 will be merged soon so mathlib will know that the kernel of aeval a is generated by the minpoly of a.

ericrbg
ericrbg approved these changes Jan 10, 2023
View reviewed changes
Copy link
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/ring_theory/power_basis.lean Show resolved Hide resolved
@Vierkantor Vierkantor self-assigned this Jan 11, 2023
Vierkantor
Vierkantor approved these changes Jan 11, 2023
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.

Nice work! It should be good to merge if you un@[simp] aeval_minpoly_gen, degree_minpoly_gen and nat_degree_minpoly_gen, and add a @[simp] lemma degree_minpoly [nontrivial A] (pb : power_basis A S) : (minpoly A pb.gen).degree = pb.dim.

bors d+

@bors
Copy link

bors bot commented Jan 11, 2023

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

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the delegated The PR author may merge after reviewing final suggestions. label Jan 11, 2023
@alreadydone
Copy link
Collaborator Author

@Vierkantor Thanks for quick approval! I did some more golfs at this commit, removing the is_integral hypothesis and namespace from linear_independent_pow, so I'll wait until you take another look before merging this.

alreadydone
alreadydone commented Jan 12, 2023
View reviewed changes
src/ring_theory/power_basis.lean
Comment on lines +426 to +427
simp only at hg,
simp_rw [algebra.smul_def, ← aeval_monomial, ← map_sum] at hg,
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

weird that we need simp only before simp_rw ...

@alreadydone alreadydone added awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 12, 2023
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 12, 2023
@alreadydone
Copy link
Collaborator Author

No comments apparently. Let me merge this then!

bors r+

bors bot pushed a commit that referenced this pull request Jan 14, 2023
@alreadydone
feat(ring_theory/power_basis): minpoly_gen is always the minimal poly…
0a6c26e 
…nomial (#18117)

+ add `minpoly.unique'`, a characterization for being the minimal polynomial.

+ golf various proofs and remove some unnecessary typeclass assumptions.
@bors
Copy link

bors bot commented Jan 14, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial [Merged by Bors] - feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial Jan 14, 2023
@bors bors bot closed this Jan 14, 2023
@bors bors bot deleted the power_basis_minpoly branch January 14, 2023 23:59
@alreadydone alreadydone restored the power_basis_minpoly branch January 15, 2023 04:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ericrbg ericrbg ericrbg approved these changes

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees

@Vierkantor Vierkantor

Labels
delegated The PR author may merge after reviewing final suggestions. t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@alreadydone @Paul-Lez @Vierkantor @ericrbg @leanprover-community-bot-assistant