conditional convergent series in lean

Stream: new members

[Chengyan Hu]

Hi! I found out that we only allow absolutely convergent series in lean. I'm curious about how should I define an infinite sum that it only convergent under some order of sum? For example, the infinite sum (-1)^n *(1/n) over positive natural number.

[Chengyan Hu]

It sounds like if we are summing over a set with order like N, we are able to talk about conditional convergent?

[Aaron Liu]

See #mathlib4 > Conditionally convergent series