∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {x : ℝ},
  MeasureTheory.Measure.map X μ = MeasureTheory.Measure.dirac x →
    ∀ (t : ℝ), ProbabilityTheory.mgf X μ t = Real.exp (x * t)