const_smul — Mathlib

English

If a scalar is central, then its right action is measurable when its left action is; i.e., the MeasurableConstSMul for the opposite action holds.

Русский

Если скаляр центральный, то правая интенция действует измеримо, когда левая действует измеримо.

LaTeX

$$$\text{MeasurableConstSMul}(M^{\mathrm{op}}, \alpha)$ under IsCentralScalar(M, α)$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem const_smul (hg : Measurable g) (c : M) : Measurable (c • g) :=
  (measurable_const_smul c).comp hg

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