Re: [isabelle] Degree of an almost everywhere constant function

The only thing I am aware of is HOL-Library.Poly_Mapping, which you are
probably aware of, seeing as it has your name at the top.


On 15/10/2020 16:41, Florian Haftmann wrote:
> Hi all,
> in certain applications (most prominently polynomials) almost everywhere
> constant functions nat => 'a play a critical role, and any almost
> everywhere constant function can be assigned a degree, i. e. the highest
> n such that for any higher n the function is constant.
> Is there any stand-alone formalizsation of this concept?
> Cheers,
> 	Florian

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.