[isabelle] Degree of an almost everywhere constant function

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?


Attachment: signature.asc
Description: OpenPGP digital signature

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