Theorems · Theorem · complex analysis
FormalMultilinearSeries.coeff_ofScalars
∀ {𝕜 : Type u_3} [inst : NontriviallyNormedField 𝕜] {p : ℕ → 𝕜} {n : ℕ},
(FormalMultilinearSeries.ofScalars 𝕜 p).coeff n = p n- Defined in
- Mathlib.Analysis.Analytic.OfScalars
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NontriviallyNormedField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- mul_oneproof · cited by 3,885
- Finset.univproof · cited by 3,473
- Finset.prod_congrproof · cited by 646
- smul_applyproof · cited by 229
- Finset.prod_const_oneproof · cited by 100
- FormalMultilinearSeries.ofScalarsstatement · cited by 68
- FormalMultilinearSeries.coeffstatement · cited by 30
- ContinuousMultilinearMap.mkPiAlgebraFinproof · cited by 29
- List.prod_ofFnproof · cited by 3
Cited by23
Results whose statement or proof uses this declaration.
- AnalyticAt.hasFPowerSeriesAtproof · cited by 7
- Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zeroproof · cited by 3
- PeriodPair.coeff_weierstrassPExceptSeriesproof · cited by 3
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3
- PeriodPair.hasFPowerSeriesOnBall_weierstrassPExceptproof · cited by 3
- AnalyticAt.analyticAt_localInverseproof · cited by 2
- Real.one_div_sub_pow_hasFPowerSeriesOnBall_zeroproof · cited by 2
- hasFPowerSeriesAt_clog_oneproof · cited by 2
- Complex.regularizedHGFunSeries_coeffproof · cited by 2
- Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zeroproof · cited by 2
- Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zeroproof · cited by 1
- PeriodPair.weierstrassPExcept_eq_tsumproof · cited by 1