∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ →
    ∀ (r : ℝ), ProbabilityTheory.HasSubgaussianMGF (fun ω => r * X ω) (⟨r ^ 2, ⋯⟩ * c) μ