Theorems · Inductive type · sequences and series
HasSummableGeomSeries
(K : Type u_4) → [NormedRing K] → Prop
A normed ring has summable geometric series if, for all ξ of norm < 1, the geometric series
∑ ξ ^ n converges. This holds both in complete normed rings and in normed fields, providing a
convenient abstraction of these two classes to avoid repeating the same proofs.
- Defined in
- Mathlib.Analysis.SpecificLimits.Normed
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- NormedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NormedRingstatement · cited by 924
Cited by65
Results whose statement or proof uses this declaration.
- summable_geometric_of_norm_lt_onestatement and proof · cited by 13
- Units.oneSubstatement and proof · cited by 9
- Units.isOpenstatement and proof · cited by 6
- hasFDerivAt_ringInversestatement and proof · cited by 5
- Units.addstatement and proof · cited by 5
- Units.val_oneSubstatement and proof · cited by 4
- hasSum_choose_mul_geometric_of_norm_lt_one'statement and proof · cited by 4
- NormedRing.inverse_one_substatement and proof · cited by 4
- Units.ofNearbystatement and proof · cited by 4
- differentiableAt_inversestatement and proof · cited by 4
- hasFPowerSeriesOnBall_inverse_one_substatement and proof · cited by 3
- analyticAt_inversestatement and proof · cited by 3