Dear HOL-Computational_Algebra developers,
how about renaming "reflect_poly" in Polynomial.thy to "reciprocal_poly"?
It seems to be standard to call them "reciprocal polynomials", cf.
https://en.wikipedia.org/wiki/Reciprocal_polynomial, and the current
naming wants an extra sentence to relate
Dear Manuel,
There are definitely books out there that call it the "reflected
polynomial", and that's what my undergraduate discrete maths course
called it, so that's what I called it.
oh I'm fine with the naming if it's textbook-level standard. I wouldn't
have raised this if there were a
Dear Alexander, Florian, Larry, Manuel,
recently I also made the same typedef, so that derivatives can be
defined, which wants real norm in current Isabelle/HOL. Unfortunately I
didn't notice it is called "poly_mapping".
I propose calling them finsupp or finite_supp. Support is often written
