α : Type u_1
β : Type ?u.620644
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
⊢ 0 = 0 + withDensityᵥ μ 0
α : Type u_1
β : Type ?u.620644
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
⊢ singularPart 0 μ = 0
refine' (eq_singularPart 0 0 VectorMeasure.MutuallySingular.zero_left _).symm
no goals
α : Type u_1
β : Type ?u.620644
m : MeasurableSpace α
μ✝ ν : Measure α
s t : SignedMeasure α
μ : Measure α
⊢ 0 = 0 + withDensityᵥ μ 0
rw [zero_add, withDensityᵥ_zero]