mathlib

4461149a - chore(algebra/geom_sum): golf a proof (#15450)