From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

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

signature.asc

From: Manuel Eberl <eberlm@in.tum.de>

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.

Manuel

signature.asc

Last updated: Jan 25 2022 at 01:11 UTC