Theorems · Theorem · complex analysis

Function.Periodic.cuspFunction_smul

∀ {h : ℝ} {f : ℂ → ℂ},
  ContinuousAt (Function.Periodic.cuspFunction h f) 0 →
    ∀ (a : ℂ), Function.Periodic.cuspFunction h (a • f) = a • Function.Periodic.cuspFunction h f

Defined in

Mathlib.Analysis.Complex.Periodic

Cited by

2 results in Mathlib

Foundations

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