∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν]
  [MeasureTheory.SigmaFinite μ] {r : ENNReal}, r ≠ 0 → r ≠ ⊤ → ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ