Document `summable` in `realsum.v`. #2067

Open

Labels

documentation 📝

Milestone

opened

on Jul 30, 2026

analysis/experimental_reals/realsum.v

Line 34 in ba95a8f

Definition summable := exists (M : R), forall (J : {fset T}),

Metadata

Assignees

No one assigned

Labels

documentation 📝

Type

No type

Projects

No projects

Milestone

1.18.0

Relationships

None yet

Development

No branches or pull requests