-
Notifications
You must be signed in to change notification settings - Fork 298
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.
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
[Merged by Bors] - feat(algebra/polynomial, data/polynomial): lemmas about monic polynomials #3402
Closed
Closed
Changes from 85 commits
Commits
Show all changes
87 commits
Select commit
Hold shift + click to select a range
057835f
init
jalex-stark 3e7cdfc
take a simpler typeclass assumption
jalex-stark 40cb3bf
Added some sorried lemmas
awainverse 8d45565
shuffled variables around, error-free now
jalex-stark 3177c74
closed sorries
jalex-stark 5bf0ce2
upgraded a lemma from integral domain to comm_semiring
jalex-stark 0de15c7
monoid_hom.map_prod?
jalex-stark 47383fb
One more sorry closed
awainverse bbd0c86
Merge branch 'poly_big_ops' of https://github.com/leanprover-communit…
awainverse 72c6191
Monoid homs are good
awainverse e856a64
Removing an old comment
awainverse cb4ba5f
tidied docstring
jalex-stark d07ad32
tidied docstring?
jalex-stark cfbf6b6
Merge branch 'poly_big_ops' of https://github.com/leanprover-communit…
jalex-stark 9bd57c4
switched a proof to use induciton tactic
jalex-stark 1528caf
another induction conversion
jalex-stark 7f6de18
Even more homs
awainverse 0fc8bc7
Merge branch 'poly_big_ops' of https://github.com/leanprover-communit…
awainverse a32da0a
Docstrings
awainverse 439068c
Linting [decidable_eq] to classical in proof
awainverse 33409ee
init
jalex-stark 22d54e4
Merge remote-tracking branch 'origin/poly_big_ops' into polynomial_le…
awainverse 2adab74
file move
jalex-stark 4e1ce77
Trimmed some things down
awainverse 5b8b8a4
narrowed scope of module docstring
jalex-stark 8f5486e
file move
jalex-stark fbbae0b
Merge branch 'poly_big_ops' into polynomial_lemmas_for_freek_83
jalex-stark 8156a81
break into two files
jalex-stark 4594ee7
split out monic.lean
jalex-stark 48372a5
break basic.lean up by level of typeclass assumption
jalex-stark 37d044b
move stuff out of big_operators not matching the module docstring
jalex-stark ca1bb99
split into two files
jalex-stark 4e94069
added more module docstring
jalex-stark a5a4f9b
changed a proof to use induction tactic
jalex-stark 2f392aa
Improving documentation
awainverse 639cd08
Noncomputable theory
awainverse a2ea03a
char_p lemmas
awainverse 1c01f6b
deduped proof of add_pow_char
jalex-stark f909e25
Update src/algebra/polynomial/basic.lean
jalex-stark cb66b41
Replaced new alg_homs with aeval
awainverse cf4cfab
Merge branch 'poly_big_ops' of https://github.com/leanprover-communit…
awainverse af2d806
coe vs. apply
awainverse 0ea52ee
Answering reviews
awainverse d380edc
made next_coeff_mul faster at the cost of sorries
jalex-stark 3de1ecf
tweaked documentation for prime lemmas
jalex-stark 4bc378d
remove sorries
jalex-stark 0207446
Update src/algebra/polynomial/basic.lean
jalex-stark 0d3698c
Update src/algebra/polynomial/basic.lean
jalex-stark 0b427ad
Update src/algebra/polynomial/basic.lean
jalex-stark 8613f00
Update src/algebra/polynomial/big_operators.lean
jalex-stark f662cbf
Update src/algebra/polynomial/big_operators.lean
jalex-stark df3acb6
tweak documentation per johan's suggestion
jalex-stark f6ced67
Merge branch 'poly_big_ops' into polynomial_lemmas_for_freek_83
jalex-stark 0f63f11
revert field_theory/finite
jalex-stark ba3927f
Update src/algebra/polynomial/basic.lean
jalex-stark cf840c9
Update src/algebra/char_p.lean
jalex-stark 644cb14
golfing
jalex-stark 28911fc
Merge branch 'polynomial_lemmas_for_freek_83' of https://github.com/l…
jalex-stark 4dd84b6
Delete big_operators.lean
jalex-stark 6f79fb7
Update src/algebra/polynomial/basic.lean
jalex-stark 1c19e29
Update src/algebra/polynomial/basic.lean
jalex-stark 4ec8427
Merge branch 'master' into polynomial_lemmas_for_freek_83
jalex-stark cf92c40
merge algebra/polynomial/basic.lean into data/polynomial/basic.lean
jalex-stark 2300452
...and actually add the code to data, in addition to reomving it from…
jalex-stark 4916f27
simplify proof
jalex-stark 5687211
merge algebra/polynomial/monic into data/polynomial/monic
jalex-stark 6114fa4
resolve a comment
jalex-stark 6226ae1
resolve a comment
jalex-stark 9ea7d32
docs
jalex-stark 7c6ff25
Update src/algebra/char_p.lean
jalex-stark 61eb1c8
formatting
jalex-stark 86d31e5
Merge branch 'polynomial_lemmas_for_freek_83' of https://github.com/l…
jalex-stark a77bd29
attempt to fix import
jalex-stark 890443c
squeeze import
jalex-stark 3314e11
expand a doc
jalex-stark 78680bf
Update src/algebra/polynomial/big_operators.lean
jalex-stark d0b1249
name changes
jalex-stark 3179603
swap for bigops notation
jalex-stark 9ac5c60
naming
jalex-stark 9b49e63
i maybe got all of them this time
jalex-stark 9303e57
Merge remote-tracking branch 'origin/master' into polynomial_lemmas_f…
jalex-stark 46b8a10
pow_eq
jalex-stark 5e138a0
restore missing tactic import
jalex-stark 586ee4d
remove zombie file
jalex-stark e46d267
...and actually remove the file
jalex-stark 4368c1d
two more name changes
jalex-stark 4c3a76d
Merge remote-tracking branch 'origin/master' into polynomial_lemmas_f…
jalex-stark File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
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 thenext_coeff
to use projection notation?