Skip to content

[Merged by Bors] - feat(Algebra/Polynomial/Bivariate): add lemmas for bivariate polynomials#14579

Closed
Multramate wants to merge 4 commits intomasterfrom
Bivariate
Closed

[Merged by Bors] - feat(Algebra/Polynomial/Bivariate): add lemmas for bivariate polynomials#14579
Multramate wants to merge 4 commits intomasterfrom
Bivariate

Conversation

@Multramate
Copy link
Copy Markdown
Collaborator

@Multramate Multramate commented Jul 9, 2024

Open in Gitpod

@Multramate Multramate added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Jul 9, 2024
@Multramate Multramate requested a review from alreadydone July 9, 2024 17:23
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 9, 2024 •
edited
Loading

PR summary 1644914045

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ evalEval_CC
+ evalEval_add
+ evalEval_dvd
+ evalEval_finset_sum
+ evalEval_intCast
+ evalEval_list_prod
+ evalEval_mul
+ evalEval_multiset_prod
+ evalEval_natCast
+ evalEval_neg
+ evalEval_one
+ evalEval_pow
+ evalEval_prod
+ evalEval_smul
+ evalEval_sub
+ evalEval_sum
+ evalEval_surjective
+ evalEval_zero

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for `script/declarations_diff.sh` contains some details about this script.

@Multramate
Copy link
Copy Markdown
Collaborator Author

Multramate commented Jul 9, 2024 •
edited
Loading

These are not strictly necessary, because we can just rewrite evalEval into eval (or into evalEvalRingHom), and apply the corresponding lemmas of eval (or of general ring maps), but are API that are "nice to have".

I noted, when doing this, that there are a few missing gaps in the API of eval, but I'll not touch them here.

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 9, 2024
kim-em
kim-em reviewed Jul 15, 2024
View reviewed changes
@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 15, 2024
@Multramate Multramate removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 15, 2024
kim-em
kim-em reviewed Jul 15, 2024
View reviewed changes
kim-em
kim-em reviewed Jul 20, 2024
View reviewed changes
Mathlib/Algebra/Polynomial/Bivariate.lean Outdated

@[simp]
lemma evalEval_ofNat (x y : R) (n : ℕ) [n.AtLeastTwo] :
(OfNat.ofNat n : R[X][Y]).evalEval x y = OfNat.ofNat n := by
Copy link
Copy Markdown
Contributor

@kim-em kim-em Jul 20, 2024

Choose a reason for hiding this comment

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

Is it necessary to write OfNat.ofNat here, rather than just n?

Copy link
Copy Markdown
Collaborator Author

@Multramate Multramate Jul 29, 2024

Choose a reason for hiding this comment

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

I copied the corresponding lemma for eval. Without the Ofnat.ofNat this is the same as evalEval_natCast.

Ruben-VandeVelde
Ruben-VandeVelde reviewed Jul 28, 2024
View reviewed changes
Mathlib/Algebra/Polynomial/Bivariate.lean Outdated

@[simp]
lemma evalEval_ofNat (x y : R) (n : ℕ) [n.AtLeastTwo] :
(OfNat.ofNat n : R[X][Y]).evalEval x y = OfNat.ofNat n := by
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde Jul 28, 2024

Choose a reason for hiding this comment

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

Does this work without no_index?

Copy link
Copy Markdown
Collaborator Author

@Multramate Multramate Jul 29, 2024

Choose a reason for hiding this comment

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

What is no_index?

jcommelin
jcommelin reviewed Aug 23, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin 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 merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Aug 23, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 23, 2024
@Multramate
feat(Algebra/Polynomial/Bivariate): add lemmas for bivariate polynomi…
1699b55 
…als (#14579)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Polynomial/Bivariate): add lemmas for bivariate polynomials [Merged by Bors] - feat(Algebra/Polynomial/Bivariate): add lemmas for bivariate polynomials Aug 23, 2024
@mathlib-bors mathlib-bors bot closed this Aug 23, 2024
@mathlib-bors mathlib-bors bot deleted the Bivariate branch August 23, 2024 04:17
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@Multramate @bjoernkjoshanssen
feat(Algebra/Polynomial/Bivariate): add lemmas for bivariate polynomi…
f036c27 
…als (#14579)
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@Multramate @bjoernkjoshanssen
feat(Algebra/Polynomial/Bivariate): add lemmas for bivariate polynomi…
a6c8e43 
…als (#14579)
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@Multramate @bjoernkjoshanssen
feat(Algebra/Polynomial/Bivariate): add lemmas for bivariate polynomi…
85fe55e 
…als (#14579)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@jcommelin jcommelin jcommelin left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

@alreadydone alreadydone Awaiting requested review from alreadydone

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@Multramate @kim-em @jcommelin @Ruben-VandeVelde