Theorem hasSummableGeomSeries_iff_isQuasiregular

Modification history

2026-09-11 08:52
Mathlib/Analysis/SpecificLimits/Normed.lean
refactor: allow non-unital normed rings in `HasSummableGeomSeries` (#43141) …
Added hasSummableGeomSeries_iff_isQuasiregularView on Github →