Zulip Chat Archive
Stream: general
Topic: bundled polynomial.eval and polynomial.eval₂
Kenny Lau (Apr 07 2020 at 07:59):
are there bundled versions of polynomial.eval and polynomial.eval₂?
Johan Commelin (Apr 07 2020 at 07:59):
I think Yury made those last week
Kenny Lau (Apr 07 2020 at 08:03):
are they in mathlib?
Johan Commelin (Apr 07 2020 at 08:03):
Not sure, I think so
Johan Commelin (Apr 07 2020 at 08:03):
Aah, no, it's still a PR maybe
Johan Commelin (Apr 07 2020 at 08:03):
Johan Commelin (Apr 07 2020 at 08:05):
@Kenny Lau maybe you can help fixing that PR?
Yury G. Kudryashov (Apr 07 2020 at 08:34):
I'll try to fix it in a few hours.
Yury G. Kudryashov (Apr 07 2020 at 08:35):
Though polynomial.eval₂_hom is already in mathlib.
Yury G. Kudryashov (Apr 07 2020 at 08:36):
Sorry, I'm wrong.
Yury G. Kudryashov (Apr 07 2020 at 08:36):
I added it for mv_polynomial but for polynomial it is a lemma
Last updated: Dec 20 2023 at 11:08 UTC