Commit 2021-09-16 11:34 8a1fc68e
View on Github →feat(measure_theory/measure/with_density_vector_measure): with_densityᵥ of a real function equals the density of the pos part - density of the neg part (#9215)
feat(measure_theory/measure/with_density_vector_measure): with_densityᵥ of a real function equals the density of the pos part - density of the neg part (#9215)