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(algebra/polynomial, data/polynomial): lemmas about monic polynomials #3402

Closed
wants to merge 87 commits into from
Closed

[Merged by Bors] - feat(algebra/polynomial, data/polynomial): lemmas about monic polynomials #3402

wants to merge 87 commits into from

Conversation

jalex-stark
Copy link
Collaborator

This does most of the heavy lifting for "the trace of a matrix is the second coefficient of its characteristic polynomial"

jalex-stark and others added 30 commits July 12, 2020 13:39
@jalex-stark
init
057835f
@jalex-stark
take a simpler typeclass assumption
3e7cdfc
@awainverse
Added some sorried lemmas
40cb3bf
@jalex-stark
shuffled variables around, error-free now
8d45565
@jalex-stark
closed sorries
3177c74
@jalex-stark
upgraded a lemma from integral domain to comm_semiring
5bf0ce2
@jalex-stark
monoid_hom.map_prod?
0de15c7
@awainverse
One more sorry closed
47383fb
@awainverse
Merge branch 'poly_big_ops' of https://github.com/leanprover-communit…
bbd0c86 
…y/mathlib into poly_big_ops
@awainverse
Monoid homs are good
72c6191
@awainverse
Removing an old comment
e856a64
@jalex-stark
tidied docstring
cb4ba5f
@jalex-stark
tidied docstring?
d07ad32
@jalex-stark
Merge branch 'poly_big_ops' of https://github.com/leanprover-communit…
cfbf6b6 
…y/mathlib into poly_big_ops
@jalex-stark
switched a proof to use induciton tactic
9bd57c4
@jalex-stark
another induction conversion
1528caf
@awainverse
Even more homs
7f6de18
@awainverse
Merge branch 'poly_big_ops' of https://github.com/leanprover-communit…
0fc8bc7 
…y/mathlib into poly_big_ops
@awainverse
Docstrings
a32da0a
@awainverse
Linting [decidable_eq] to classical in proof
439068c
@jalex-stark
init
33409ee
@awainverse
Merge remote-tracking branch 'origin/poly_big_ops' into polynomial_le…
22d54e4 
…mmas_for_freek_83
@jalex-stark
file move
2adab74
@awainverse
Trimmed some things down
4e1ce77
@jalex-stark
narrowed scope of module docstring
5b8b8a4
@jalex-stark
file move
8f5486e
@jalex-stark
Merge branch 'poly_big_ops' into polynomial_lemmas_for_freek_83
fbbae0b
@jalex-stark
break into two files
8156a81
@jalex-stark
split out monic.lean
4594ee7
@jalex-stark
break basic.lean up by level of typeclass assumption
48372a5
@jalex-stark
Copy link
Collaborator Author

I'd like to check the naming more thoroughly (or someone else to say they've done so), but I should run for now.

I did a closer pass at the names. I got rid of all the *_eq names (which are old, so now this PR touches several more files), and I applied Scott's suggestion for renaming monic.degree_one. The rest of the names seem okay to me, with maybe the fishiest one being card_pred_coeff_prod_X_sub_C.

@jalex-stark jalex-stark 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 Jul 17, 2020
semorrison
semorrison reviewed Jul 18, 2020
View reviewed changes
src/algebra/polynomial/big_operators.lean Outdated
Comment on lines 91 to 92
lemma next_coeff_prod_X_sub_C [nontrivial R] {s : finset ι} (f : ι → R) :
next_coeff ∏ i in s, (X - C (f i)) = -∑ i in s, f i :=
Copy link
Collaborator

Choose a reason for hiding this comment

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

Maybe easier to find as prod_X_sub_C_next_coeff? Can you move the next_coeff to use projection notation?

@semorrison
Copy link
Collaborator

After that, I think we're good to go! Thanks!

bors d+

@bors
Copy link

bors bot commented Jul 18, 2020

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

@semorrison semorrison 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 awaiting-author A reviewer has asked the author a question or requested changes labels Jul 18, 2020
@jalex-stark
Copy link
Collaborator Author

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

bors r+

bors bot pushed a commit that referenced this pull request Jul 18, 2020
@jalex-stark @awainverse
feat(algebra/polynomial, data/polynomial): lemmas about monic polynom…
4850427 
…ials (#3402)




Co-authored-by: Aaron Anderson <awainverse@gmail.com>
@bors
Copy link

bors bot commented Jul 18, 2020

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jul 18, 2020
@jalex-stark @awainverse
feat(algebra/polynomial, data/polynomial): lemmas about monic polynom…
ea749ae 
…ials (#3402)




Co-authored-by: Aaron Anderson <awainverse@gmail.com>
@bors
Copy link

bors bot commented Jul 18, 2020

Canceled.

@jalex-stark
Copy link
Collaborator Author

Build failed (retrying...):

It's failing here

/home/runner/work/mathlib/mathlib/src/ring_theory/polynomial_algebra.lean:135:2: error: unknown identifier 'apply_eq_coeff'

which is confusing to me because that file just compiles on my machine.

@bryangingechen
Copy link
Collaborator

I think the build failure may have been due to #3420 which was in the same batch.
bors r+

@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 Jul 18, 2020
bors bot pushed a commit that referenced this pull request Jul 18, 2020
@jalex-stark @awainverse
feat(algebra/polynomial, data/polynomial): lemmas about monic polynom…
4760a33 
…ials (#3402)




Co-authored-by: Aaron Anderson <awainverse@gmail.com>
@bors
Copy link

bors bot commented Jul 18, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/polynomial, data/polynomial): lemmas about monic polynomials [Merged by Bors] - feat(algebra/polynomial, data/polynomial): lemmas about monic polynomials Jul 18, 2020
@bors bors bot closed this Jul 18, 2020
@bors bors bot deleted the polynomial_lemmas_for_freek_83 branch July 18, 2020 17:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
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
5 participants
@jalex-stark @jcommelin @bryangingechen @semorrison @awainverse