case a
α : Type u_1
β : Type ?u.74138
inst✝ : MeasurableSpace α
⊢ toSignedMeasure (toJordanDecomposition 0) = toSignedMeasure 0
α : Type u_1
β : Type ?u.74138
inst✝ : MeasurableSpace α
⊢ toJordanDecomposition 0 = 0
apply toSignedMeasure_injective
no goals
case a
α : Type u_1
β : Type ?u.74138
inst✝ : MeasurableSpace α
⊢ toSignedMeasure (toJordanDecomposition 0) = toSignedMeasure 0
simp [toSignedMeasure_zero]