Theorems · Theorem · abstract harmonic analysis

DiscreteConvolution.addConvolution_indicator_zero_right

∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_6} [inst : AddMonoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid F] [inst_4 : Module S E] [inst_5 : Module S F]
  [inst_6 : TopologicalSpace F] (L : F →ₗ[S] E →ₗ[S] F) (f : M → F) (e : E),
  (∀ (y : F), (L y) e = y) → DiscreteConvolution.addConvolution L f ({0}.indicator fun x => e) = f

Defined in

Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddMonoidCommSemiringAddCommMonoidAddCommMonoidModuleModuleTopologicalSpace