[Merged by Bors] - feat(data/polynomial): lemma about aeval on functions, and on subalgebras #7252
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This also renames some variables from α to R for readability
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…thlib into aeval_subalgebra
github-actions
bot
added
the
blocked-by-other-PR
github-actions
bot
removed
the
blocked-by-other-PR
|
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
semorrison
added
the
awaiting-review
|
Can you merge master again to shrink the diff? (Or better; rebase, it will reduce the build time) |
|
@eric-wieser, why would rebasing make a difference to build time? It's unfortunate if there's an advantage there, because other times we've discouraged people from force-pushing to PRs. |
|
Because CI pulls its cache from the chain of first parents. If you rebase, that first parent is |
|
For PRs that touch Note that creating the merge commit with the parents "backwards" is probably not a good idea either, as that can confuse github. |
| @@ -119,7 +119,7 @@ alg_hom.map_zero (aeval x) | |||
|
|
|||
| @[simp] lemma aeval_C (r : R) : aeval x (C r) = algebra_map R A r := eval₂_C _ x | |||
|
|
|||
| lemma aeval_monomial {n : ℕ} {r : R} : aeval x (monomial n r) = (algebra_map _ _ r) * x^n := | |||
| @[simp] lemma aeval_monomial {n : ℕ} {r : R} : aeval x (monomial n r) = (algebra_map _ _ r) * x^n := | |||
There was a problem hiding this comment.
Hmm, should the right hand side of this lemma also be in terms of monomial?
github-actions
bot
added
ready-to-merge
…bras (#7252) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Prerequisites PR for Stone-Weierstrass.