English
The MeasurableSMul instance for the opposite multiplication Mᵐᵒᵖ on α is defined via op and unop.
Русский
Inst MeasurableSMul для противоположной умножения Mᵐᵒᵖ на α задан через op и unop.
LaTeX
$$$\\text{MeasurableSMul }(MulOpposite\\,M)\\alpha$$$
Lean4
/-- If a scalar is central, then its right action is measurable when its left action is. -/
@[to_additive]
nonrec instance op {M α} [MeasurableSpace M] [MeasurableSpace α] [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α]
[MeasurableSMul M α] : MeasurableSMul Mᵐᵒᵖ α where
measurable_smul_const
x :=
show Measurable fun c => op (unop c) • x by
simpa only [op_smul_eq_smul] using (measurable_smul_const x).comp measurable_mul_unop
