Structures · Analysis
HasSummableGeomSeries
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
- Shape
- One type argument · adds summable_geometric_of_norm_lt_one
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by64
- summable_geometric_of_norm_lt_one
- Units.oneSub
- Units.isOpen
- Units.add
- hasFDerivAt_ringInverse
- differentiableAt_inverse
- hasSum_choose_mul_geometric_of_norm_lt_one'
- NormedRing.inverse_one_sub
- Units.ofNearby
- Units.val_oneSub
- hasFPowerSeriesOnBall_inverse_one_sub
- NormedRing.inverse_continuousAt
- analyticAt_inverse
- NormedRing.inverse_add_norm_diff_nth_order
- hasSum_coe_mul_geometric_of_norm_lt_one'
- geom_series_succ
- Units.val_add
- NormedRing.inverse_add
- nonunits.isClosed
- hasSum_geom_series_inverse
- Units.isOpenEmbedding_val
- hasFPowerSeriesOnBall_inverse_one_add
- NormedRing.inverse_one_sub_norm
- contDiffAt_ringInverse
- summable_descFactorial_mul_geometric_of_norm_lt_one
- HasSummableGeomSeries.summable_geometric_of_norm_lt_one
- NormedRing.inverse_one_sub_nth_order
- NormedRing.inverse_add_norm
- DifferentiableWithinAt.inverse
- differentiableWithinAt_inverse
- summable_pow_mul_geometric_of_norm_lt_one
- analyticAt_inverse_one_sub
- spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul
- geom_series_mul_shift
- NormedRing.inverse_add_norm_diff_first_order
- NormedRing.inverse_add_nth_order
- analyticOnNhd_inverse
- Units.oneSub.congr_simp
- NormedRing.inverse_add_norm_diff_second_order
- geom_series_mul_one_add
- DifferentiableAt.inverse
- geom_series_eq_inverse
- isUnit_one_sub_of_norm_lt_one
- fderiv_inverse
- NormedRing.inverse_one_sub_nth_order'
- hasStrictFDerivAt_ringInverse
- Ideal.closure_ne_top
- summable_choose_mul_geometric_of_norm_lt_one
- mul_neg_geom_series
- Units.val_ofNearby
Ancestors0
No ancestors.