Theorems · Theorem · several complex variables
analyticAt_inverse_one_sub
∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A] [HasSummableGeomSeries A], AnalyticAt 𝕜 (fun x => Ring.inverse (1 - x)) 0
- Defined in
- Mathlib.Analysis.Analytic.Constructions
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- NormedAlgebrastatement and proof · cited by 1,165
- NormedRingstatement and proof · cited by 924
- AnalyticAtstatement · cited by 321
- Ring.inversestatement · cited by 160
- HasSummableGeomSeriesstatement and proof · cited by 60
- formalMultilinearSeries_geometricproof · cited by 12
- hasFPowerSeriesOnBall_inverse_one_subproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- analyticAt_inverseproof · cited by 3