measurableSMul_opposite_of_mul — Mathlib

English

The action of units on β is measurable as a SMul operation, i.e., MeasurableSMul (Units M) β.

Русский

Действие единиц на β измеримо как операция SMul: MeasurableSMul (Units M) β.

LaTeX

$$$\\text{MeasurableSMul }(Units\\,M)\\beta$$$

Lean4

@[to_additive]
instance measurableSMul_opposite_of_mul {M : Type*} [Mul M] [MeasurableSpace M] [MeasurableMul M] :
    MeasurableSMul Mᵐᵒᵖ M where
  measurable_const_smul c := measurable_mul_const (unop c)
  measurable_smul_const x := measurable_mul_unop.const_mul x

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