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

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

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.

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