Theorems · Theorem · integral transforms

MellinConvergent.const_smul

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {s : ℂ},
  MellinConvergent f s →
    ∀ {𝕜 : Type u_2} [inst_2 : NormedAddCommGroup 𝕜] [inst_3 : SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E]
      [SMulCommClass ℂ 𝕜 E] (c : 𝕜), MellinConvergent (fun t => c • f t) s

Defined in

Mathlib.Analysis.MellinTransform

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupSMulZeroClassIsBoundedSMulSMulCommClass