smul_convolution — Mathlib

English

If the scalar field commutes suitably with the target space, then y·f ⋆ g = f ⋆ (y·g) and analogous rules hold.

Русский

Если скалярное поле совмещается над целевым пространством, выполняются правильные тождества: y·(f⋆g) = (y·f)⋆g и т.д.

LaTeX

$$$y\\cdot (f⋆[L,μ]g)=(y\\cdot f)⋆[L,μ]g$$$

Lean4

theorem smul_convolution [SMulCommClass ℝ 𝕜 F] {y : 𝕜} : y • f ⋆[L, μ] g = y • (f ⋆[L, μ] g) := by ext;
  simp only [Pi.smul_apply, convolution_def, ← integral_smul, L.map_smul₂]

Похожие утверждения