Theorems · Theorem · several complex variables
analyticAt_inverse
∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {A : Type u_7} [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
[HasSummableGeomSeries A] (z : Aˣ), AnalyticAt 𝕜 Ring.inverse ↑zIf A is a normed algebra over 𝕜 with summable geometric series, then inversion on A is
analytic at any unit.
- Defined in
- Mathlib.Analysis.Analytic.Constructions
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites46
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NormedAddCommGroupproof · cited by 15,752
- NormedSpaceproof · cited by 12,499
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- nhdsproof · cited by 5,554
- Norm.normproof · cited by 5,413
- Filter.Eventuallyproof · cited by 3,134
- Unitsstatement and proof · cited by 2,804
- Nontrivialproof · cited by 2,416
- Units.valstatement and proof · cited by 1,966
- Filter.univ_mem'proof · cited by 1,672
- Filter.mp_memproof · cited by 1,537
- NormedAlgebrastatement and proof · cited by 1,165
Cited by3
Results whose statement or proof uses this declaration.
- analyticAt_invproof · cited by 3
- analyticOnNhd_inverseproof · cited by 1
- hasStrictFDerivAt_ringInverseproof · cited by 1