case a
α : Type u_1
β : Type ?u.75261
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ toSignedMeasure (toJordanDecomposition (r • s)) = toSignedMeasure (r • toJordanDecomposition s)
α : Type u_1
β : Type ?u.75261
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ toJordanDecomposition (r • s) = r • toJordanDecomposition s
apply toSignedMeasure_injective
no goals
case a
α : Type u_1
β : Type ?u.75261
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ toSignedMeasure (toJordanDecomposition (r • s)) = toSignedMeasure (r • toJordanDecomposition s)
simp [toSignedMeasure_smul]