Commit 2026-09-11 08:52 7df26f74

refactor: allow non-unital normed rings in HasSummableGeomSeries (#43141) This PR changes the field of HasSummableGeomSeries to a version which is equivalent for NormedRings, but which also makes sense and is useful in NonUnitalNormedRings. In particular, the previous definition was, for x : R and ‖x‖ < 1: Summable (fun n : ℕ ↦ x ^ n), which doesn't work for non-unital rings since there is no Pow R ℕ instance. We change the field to Summable (fun n : ℕ ↦ (· * x)^[n] x) (i.e., fun n ↦ x ^ (n + 1)). We are forced to use iterated multiplication because Mathlib currently doesn't define any Pow G ℕ+ instance for semigroups G, however, when it eventually does, we can switch this definition easily to make use of that instead. In addition to this change, we show the HasSummableGeomSeries is equivalent (in non-unital normed rings) to every element of the open unit ball being quasiregular, and consequently (in normed rings) to every element x of the open unit ball satisfying IsUnit (1 - x). These changes are used in other PRs (see #42779 and #42782):

1. to show that HasSummableGeomSeries is preserved under A ↦ WithLp 1 (Unitization 𝕜 A)
2. to provide some mild generalization of results on the quasispectrum in non-unital Banach algebras
3. remove some NormOneClass assumptions for some results on the spectrum in unital Banach algebras