search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
203 stars 45 forks source link

status of the file `summability.v` #1284

Closed affeldt-aist closed 1 month ago

affeldt-aist commented 2 months ago

https://github.com/math-comp/analysis/blob/master/theories/summability.v

Since this file is not really used yet, it can maybe be moved to the showcase subdirectory?

@CohenCyril @strub

CohenCyril commented 2 months ago

This https://github.com/math-comp/analysis/blob/cc30e18836e5772db55322fe348ade6188e1d324/theories/summability.v#L46-L49 is a candidate replacement, more idiomatic to mathcomp analysis, for https://github.com/math-comp/analysis/blob/cc30e18836e5772db55322fe348ade6188e1d324/theories/altreals/realsum.v#L31-L32

It could be removed and replaced by an issue :shrug:

affeldt-aist commented 2 months ago

Or move to realsum.v and kept in a module near the definition it could replace?