search

math-comp / trajectories

0 stars 4 forks source link

translate_pol' #1

Closed affeldt-aist closed 2 years ago

affeldt-aist commented 2 years ago

https://github.com/affeldt-aist/trajectories/blob/d7eddd45c917c1d7e628d901bd494dd2253763a5/theories/ssr_descartes/bern.v#L55

Where is it defined? @ybertot

affeldt-aist commented 2 years ago

Maybe this definition:

Definition translate_pol' (l : seq rat) (a : rat) :=
   mkseq (fun i : nat =>
     \sum_(k < (size l).+1) Qbin k i * nth 0 l k * a ^+ (k - i)) (size l).

or (size l)?