Theorems · Theorem · sequences and series
tsum_geometric_of_norm_lt_one
∀ {K : Type u_4} [inst : NormedDivisionRing K] {ξ : K}, ‖ξ‖ < 1 → ∑' (n : ℕ), ξ ^ n = (1 - ξ)⁻¹- Defined in
- Mathlib.Analysis.SpecificLimits.Normed
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedDivisionRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- SummationFilter.unconditionalstatement · cited by 2,068
- tsumstatement · cited by 1,148
- NormedDivisionRingstatement and proof · cited by 360
- HasSum.tsum_eqproof · cited by 150
- hasSum_geometric_of_norm_lt_oneproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- EulerProduct.one_sub_inv_eq_geometric_of_summable_normproof · cited by 2
- pi_mul_cot_pi_q_expproof · cited by 1
- tsum_pow_div_one_sub_eq_tsum_sigmaproof · cited by 1
- tsum_geometric_of_abs_lt_oneproof · cited by 0
- tendsto_zero_geometric_tsum_pnatproof · cited by 0