Polynomial.int

Stream: Is there code for X?

[Violeta Hernández]

I was just about to submit an entire PR duplicating this material, until I randomly stumbled upon docs#Polynomial.int. Why is it called that? I don't think I'm at fault for thinking Polynomial.int would have something to do with integers.

What about renaming it to something like Polynomial.toSubring?

[Violeta Hernández]

(meant to post this in #mathlib4, sorry)

[Violeta Hernández]

...oh, so we actually had this twice already! docs#Polynomial.toSubring

[Yaël Dillies]

I guess the name comes from the use case of restricting a polynomial with coefficients in a valued field to have coefficients in the integers of that field? But I agree it is a poor name

[Kevin Buzzard]

Or a number field!

[Violeta Hernández]

So docs#Polynomial.int has much nicer def-eqs, while docs#Polynomial.toSubring has more API and is more general. I'll make a PR merging both.

[Violeta Hernández]

#34650 redefines Polynomial.toSubring to match Polynomial.int (and moves it to a new file so people can hopefully find this easier!)