Theorems · Definition · sequences and series
Units.oneSub
{R : Type u_4} → [inst : NormedRing R] → [HasSummableGeomSeries R] → (t : R) → ‖t‖ < 1 → RˣIn a normed ring with summable geometric series, a perturbation of 1 by an element t
of distance less than 1 from 1 is a unit. Here we construct its Units structure.
- Defined in
- Mathlib.Analysis.SpecificLimits.Normed
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Norm.normstatement and proof · cited by 5,413
- Unitsstatement · cited by 2,804
- SummationFilter.unconditionalproof · cited by 2,068
- tsumproof · cited by 1,148
- NormedRingstatement and proof · cited by 924
- HasSummableGeomSeriesstatement and proof · cited by 60
- mul_neg_geom_seriesproof · cited by 0
- geom_series_mul_negproof · cited by 0
Cited by10
Results whose statement or proof uses this declaration.
- Units.addproof · cited by 5
- NormedRing.inverse_one_substatement and proof · cited by 4
- Units.val_oneSubstatement and proof · cited by 4
- analyticAt_inverseproof · cited by 3
- NormedRing.inverse_addproof · cited by 2
- isUnit_one_sub_of_norm_lt_oneproof · cited by 1
- geom_series_eq_inverseproof · cited by 1
- Units.oneSub.congr_simpstatement and proof · cited by 1
- nonunits.subset_compl_ballproof · cited by 0
- Ideal.eq_top_of_norm_lt_oneproof · cited by 0