Zulip Chat Archive

Stream: general

Topic: bundled polynomial.eval and polynomial.eval₂


view this post on Zulip Kenny Lau (Apr 07 2020 at 07:59):

are there bundled versions of polynomial.eval and polynomial.eval₂?

view this post on Zulip Johan Commelin (Apr 07 2020 at 07:59):

I think Yury made those last week

view this post on Zulip Kenny Lau (Apr 07 2020 at 08:03):

are they in mathlib?

view this post on Zulip Johan Commelin (Apr 07 2020 at 08:03):

Not sure, I think so

view this post on Zulip Johan Commelin (Apr 07 2020 at 08:03):

Aah, no, it's still a PR maybe

view this post on Zulip Johan Commelin (Apr 07 2020 at 08:03):

#2303

view this post on Zulip Johan Commelin (Apr 07 2020 at 08:05):

@Kenny Lau maybe you can help fixing that PR?

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 08:34):

I'll try to fix it in a few hours.

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 08:35):

Though polynomial.eval₂_hom is already in mathlib.

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 08:36):

Sorry, I'm wrong.

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 08:36):

I added it for mv_polynomial but for polynomial it is a lemma


Last updated: May 14 2021 at 13:24 UTC