Commit 2025-02-07 14:22 d03b769f

View on Github →

chore(Convolution): fix lemma names (#21504) From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

Modified Mathlib/Analysis/Convolution.lean

deleted theorem HasCompactSupport.convolutionExistsLeft

deleted theorem HasCompactSupport.convolutionExistsRightOfContinuousLeft

added theorem HasCompactSupport.convolutionExists_left

added theorem HasCompactSupport.convolutionExists_right_of_continuous_left

deleted theorem MeasureTheory.ConvolutionExistsAt.ofNorm'

deleted theorem MeasureTheory.ConvolutionExistsAt.ofNorm

added theorem MeasureTheory.ConvolutionExistsAt.of_norm'

added theorem MeasureTheory.ConvolutionExistsAt.of_norm