case intro
α : Type u_1
β : Type ?u.78208
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ toJordanDecomposition (↑r • s) = ↑r • toJordanDecomposition s
α : Type u_1
β : Type ?u.78208
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ toJordanDecomposition (r • s) = r • toJordanDecomposition s
lift r to ℝ≥0 using hr
case intro
α : Type u_1
β : Type ?u.78208
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ toJordanDecomposition (↑r • s) = toJordanDecomposition (r • s)
case intro
α : Type u_1
β : Type ?u.78208
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ toJordanDecomposition (↑r • s) = ↑r • toJordanDecomposition s
rw [JordanDecomposition.coe_smul, ← toJordanDecomposition_smul]
no goals
case intro
α : Type u_1
β : Type ?u.78208
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ toJordanDecomposition (↑r • s) = toJordanDecomposition (r • s)
rfl