Stream: math-comp analysis

Topic: ereals and Rbar

Dubravka Kutlesic (Nov 10 2021 at 17:24):

can I reuse anything proven with Rbar if i use ereal?

Notification Bot (Nov 10 2021 at 17:29):

This topic was moved here from #math-comp users > fold property in a sum using bigop by Karl Palmskog

Reynald Affeldt (Nov 10 2021 at 23:17):

As far as I know, the definition of the data structure is the same, so it should be possible. On the other hand, you may want to double-check how the arithmetic operations are defined in both cases.

Pierre Roux (Nov 11 2021 at 13:47):

If Rbar is the one defined in Coquelicot, the definition of the addition for instance is not exactly the same (addition over Rbar in Coquelicot is not associative for instance)

Last updated: Feb 05 2023 at 06:28 UTC