Theorems · Theorem · complex analysis

FormalMultilinearSeries.const_smul_sum_apply

∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : ContinuousConstSMul 𝕜 E]
  [inst_10 : ContinuousConstSMul 𝕜 F] {𝕜' : Type} [inst_11 : DivisionSemiring 𝕜'] [inst_12 : Module 𝕜' F]
  [inst_13 : ContinuousConstSMul 𝕜' F] [inst_14 : SMulCommClass 𝕜 𝕜' F] [T2Space F] (a : 𝕜')
  (f : FormalMultilinearSeries 𝕜 E F) (z : E), a • f.sum z = (a • f).sum z

Defined in

Mathlib.Analysis.Analytic.ConvergenceRadius

Cited by

2 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModuleTopologicalSpaceTopologicalSpaceContinuousAddContinuousAddContinuousConstSMulContinuousConstSMulDivisionSemiringModuleContinuousConstSMulSMulCommClassT2Space