mconv_comm — Mathlib

English

If the multiplication in M is commutative, then μ ∗ₘ ν = ν ∗ₘ μ.

Русский

При коммутативности умножения в M свёртка коммутирует: μ ∗ₘ ν = ν ∗ₘ μ.

LaTeX

$$$ μ ∗ₘ ν = ν ∗ₘ μ $$$

Lean4

/-- To get commutativity, we need the underlying multiplication to be commutative. -/
@[to_additive /-- To get commutativity, we need the underlying addition to be commutative. -/
    ]
theorem mconv_comm {M : Type*} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M)
    [SFinite μ] [SFinite ν] : μ ∗ₘ ν = ν ∗ₘ μ := by
  unfold mconv
  rw [← prod_swap, map_map (by fun_prop)]
  · simp [Function.comp_def, mul_comm]
  fun_prop

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