Post #1733534

@jdw Ah, nice. The following is a bit of a tangent, but this makes me think of my recent (constructivist) problem with rings, a much more elementary one. I am starting with some nonconstructive proofs which make extensive use of sums of finitely supported sets of elements of the ring. My choices as far as I can see are to restrict myself to discrete rings (don't think I'd need strongly discrete for this) or to finite sums. I've been choosing the latter although I guess either one would work for my current purposes.