∀ {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} [inst : NormedAddCommGroup F] {x : G} [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_4 : NormedSpace ℝ F]
  [inst_5 : AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] {f : G → 𝕜}
  {g : G → F}, MeasureTheory.convolution f g (ContinuousLinearMap.lsmul 𝕜 𝕜) μ x = ∫ (t : G), f (x - t) • g t ∂μ