English
If each coordinate α_i has MeasurableConstSMul by M, then the Pi-type has MeasurableConstSMul by M.
Русский
Если у каждого координата α_i есть MeasurableConstSMul M, то Pi-тип имеет MeasurableConstSMul M.
LaTeX
$$$\text{Pi inst MeasurableConstSMul}$$$
Lean4
/-- `SubNegMonoid.SMulInt` is measurable. -/
instance measurableSMul_int₂ (M : Type*) [SubNegMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] [MeasurableNeg M] :
MeasurableSMul₂ ℤ M :=
⟨by
suffices Measurable fun p : M × ℤ => p.2 • p.1 by apply this.comp measurable_swap
refine measurable_from_prod_countable_left fun n => ?_
cases n with
| ofNat n =>
simp only [Int.ofNat_eq_coe, natCast_zsmul]
exact measurable_const_smul _
| negSucc n =>
simp only [negSucc_zsmul]
exact (measurable_const_smul _).neg⟩
