Stream: math-comp analysis

Topic: ereals and Rbar

view this post on Zulip Dubravka Kutlesic (Nov 10 2021 at 17:24):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: Jun 22 2024 at 15:01 UTC