mathlib3

dc7ab9e7 - feat(measure_theory/measure/finite_measure_weak_convergence): Add some missing API lemmas. (#15205)

feat(measure_theory/measure/finite_measure_weak_convergence): Add some missing API lemmas. (#15205) Add API lemmas about extentionality of `finite_measure` and `probability_measure`, about `0 : finite_measure X`, and about scalar multiplication on `finite_measure`. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>