`BookProof.ChapterLpScaleMeasure.isProbabilityMeasure_inv_smul` [IsFiniteMeasure nu] (hne : nu Set.univ ≠ 0) : IsProbabilityMeasure ((nu Set.univ)⁻¹ • nu)

Initializing...

`BookProof.ChapterLpScaleMeasure.isProbabilityMeasure_inv_smul` [IsFiniteMeasure nu] (hne : nu Set.univ ≠ 0) : IsProbabilityMeasure ((nu Set.univ)⁻¹ • nu) · Prove2Me