Theorems · Theorem · complex analysis

circleIntegral.integral_smul

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {𝕜 : Type u_2} [inst_2 : RCLike 𝕜]
  [inst_3 : NormedSpace 𝕜 E] [SMulCommClass 𝕜 ℂ E] (a : 𝕜) (f : ℂ → E) (c : ℂ) (R : ℝ),
  ∮ (z : ℂ) in C(c, R), a • f z = a • ∮ (z : ℂ) in C(c, R), f z

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceRCLikeNormedSpaceSMulCommClass