poly

Stream: general

[Yaël Dillies]

Should docs#poly be namespaced/renamed? The name is terribly generic.

[Yaël Dillies]

Also, why are docs#poly.zero, docs#poly.one... not directly wrapped in has_zero, has_one instances?

[Alex J. Best]

That file is incredibly old and could probably do with a big review and rewrite after 5 years of mathlib progress

[Yaël Dillies]

poly.one: "The zero polynomial". Whoops :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

Oh yeah this is Mario's demonstration that you can do a bunch of Matiyesevich stuff. I remember at the time thinking that this was evidence that the software had a lot of potential. It's mathlib 2017, you don't see too many of them (other than files which were in core Lean and were moved to mathlib after the community fork, but that's not the case here). It's also probably a leaf file, it was a one off experiment which nobody built on so it's not like finset which was also there in 2017 but which has had a sustained amount of interest and love since then

[Yaël Dillies]

I'm upgrading all the fun_like-related material.

[Yaël Dillies]

Actually, the correct refactor is to use mv_polynomial in place of poly. Sounds like pain...

[Yaël Dillies]

#13403