Mathlib Map

Theorems · Definition · functional analysis

TemperedDistribution.derivCLM

(F : Type u_4) →
  [inst : AddCommGroup F] →
    [inst_1 : Module ℂ F] →
      [inst_2 : TopologicalSpace F] →
        [inst_3 : IsTopologicalAddGroup F] →
          [inst_4 : ContinuousConstSMul ℂ F] → TemperedDistribution ℝ F →L[ℂ] TemperedDistribution ℝ F

The 1-dimensional derivative on tempered distribution as a continuous ℂ-linear map.

Defined in
Mathlib.Analysis.Distribution.TemperedDistribution
Cited by
2 results in Mathlib
Foundations
Depth 226 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousConstSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

TemperedDistribution.derivCLM_apply_apply · cited by 0TemperedDistribution.deri…TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq · cited by 0TemperedDistribution.deri…Set · cited by 53352SetReal · cited by 25697RealTopologicalSpace · cited by 24529TopologicalSpaceModule · cited by 20661ModuleRingHom.id · cited by 18349RingHom.idAddCommGroup · cited by 12871AddCommGroupSet.Elem · cited by 7166Set.ElemSet.ofPred · cited by 6101Set.ofPredComplex · cited by 5565ComplexContinuousLinearMap · cited by 5352ContinuousLinearMapFinite · cited by 3029FiniteIsTopologicalAddGroup · cited by 1394IsTopologicalAddGroupContinuousConstSMul · cited by 832ContinuousConstSMulSchwartzMap · cited by 251SchwartzMapTemperedDistribution · cited by 93TemperedDistributionTemperedDistribution.derivCLMCITED BYCITES

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.