mathlib3

eec4b70c - feat(algebra/geom_sum): criteria for 0 < geom_sum (#10567)

feat(algebra/geom_sum): criteria for 0 < geom_sum (#10567) Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Johan Commelin <johan@commelin.net>