Theorems · Definition · complex analysis
FormalMultilinearSeries.ofScalarsSum
{𝕜 : Type u_1} →
{E : Type u_2} →
[inst : Field 𝕜] →
[inst_1 : Ring E] → [Algebra 𝕜 E] → [inst : TopologicalSpace E] → [IsTopologicalRing E] → (ℕ → 𝕜) → E → EThe sum of the formal power series. Takes the value 0 outside the radius of convergence.
- Defined in
- Mathlib.Analysis.Analytic.OfScalars
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- TopologicalSpacestatement and proof · cited by 24,529
- Algebrastatement and proof · cited by 11,388
- Ringstatement and proof · cited by 7,463
- Fieldstatement and proof · cited by 7,404
- IsTopologicalRingstatement and proof · cited by 402
- FormalMultilinearSeries.ofScalarsproof · cited by 68
- FormalMultilinearSeries.sumproof · cited by 34
Cited by8
Results whose statement or proof uses this declaration.
- FormalMultilinearSeries.ofScalars_sum_eqstatement · cited by 3
- FormalMultilinearSeries.ofScalarsSum_eq_tsumstatement · cited by 2
- FormalMultilinearSeries.ofScalarsSum.congr_simpstatement and proof · cited by 1
- NormedSpace.exp_eq_ofScalarsSumstatement and proof · cited by 0
- FormalMultilinearSeries.ofScalarsSum_of_subsingletonstatement and proof · cited by 0
- FormalMultilinearSeries.ofScalarsSum_opstatement · cited by 0
- FormalMultilinearSeries.ofScalarsSum_unopstatement · cited by 0
- FormalMultilinearSeries.ofScalarsSum_zerostatement · cited by 0